[STATEMENT]
lemma Aenc_synth_eq2 [simp]:
     "X \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)
[PROOF STEP]
by blast