[STATEMENT]
lemma Oops2_not_AKcryptSK:
     "\<lbrakk> evs \<in> kerbV;
         Says Tgs A \<lbrace>Crypt authK
                     \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
           \<in> set evs \<rbrakk>
      \<Longrightarrow> \<not> AKcryptSK servK SK evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs \<in> kerbV; Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> \<not> AKcryptSK servK SK evs
[PROOF STEP]
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)