[STATEMENT]
lemma has_locks_lock_lock_conv' [simp]:
  "\<lbrakk> may_lock l t'; t \<noteq> t' \<rbrakk> \<Longrightarrow> has_locks (lock_lock l t') t = has_locks l t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>may_lock l t'; t \<noteq> t'\<rbrakk> \<Longrightarrow> has_locks (lock_lock l t') t = has_locks l t
[PROOF STEP]
by(cases l)(auto elim: may_lock.cases)