[STATEMENT]
lemma Spy_analz_shrK [simp]:
     "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> woolam \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)
[PROOF STEP]
by auto