[STATEMENT]
lemma m3_inv1_lkeysec_for_analz [simp]:
  "\<lbrakk> s \<in> m3_inv1_lkeysec \<rbrakk> \<Longrightarrow> Key (shrK C) \<in> analz (IK s) \<longleftrightarrow> C \<in> bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> m3_inv1_lkeysec \<Longrightarrow> (Key (shrK C) \<in> analz (IK s)) = (C \<in> bad)
[PROOF STEP]
by auto