[STATEMENT]
lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs
[PROOF STEP]
apply (rule Nonce_supply_lemma [THEN exE])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>n\<ge>x. Nonce n \<notin> used ?evs1 \<Longrightarrow> Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs
[PROOF STEP]
apply (rule someI, fast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done