[STATEMENT]
lemma Nonce_notin_kparts [simplified]: "Guard n Ks H \<Longrightarrow> Nonce n \<notin> kparts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Guard n Ks H \<Longrightarrow> Nonce n \<notin> kparts H
[PROOF STEP]
by (auto simp: Guard_def dest: in_kparts Nonce_notin_kparts_msg)