[STATEMENT]
lemma pr_ext_agrk_user_1 [rule_format]:
 "(evs, S, A, U) \<in> protocol \<Longrightarrow>
    User m \<noteq> Spy \<longrightarrow>
    Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e)) \<in> set evs \<longrightarrow>
  ExtAgrK (S (User m, n, run)) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evs, S, A, U) \<in> protocol \<Longrightarrow> User m \<noteq> Spy \<longrightarrow> Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e)) \<in> set evs \<longrightarrow> ExtAgrK (S (User m, n, run)) \<noteq> None
[PROOF STEP]
by (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all)