Require Refine.

Parameter __term_witness : term.

Remark rem_1 : (_x1:term)(_x2:term)(_x3:term)(__aux_8 (cons _x2 (cons _x3 nil))) -> (__aux_7 _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_33 _x1 _x2 _x3 (alice_sends_message_1_to_server ? ? ? ?)); Assumption.
Qed.

Remark rem_2 : (_x1:term)(_x2:term)(_x3:term)(__aux_10 (cons _x3 nil)) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_1 _x1 _x2 _x3 (alice_sends_message_1_to_server_2 ? ? ? ?) ?); Assumption.
Qed.

Remark rem_3 : (_x1:term)(_x2:term)(_x3:term)(__aux_12 nil) -> (__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_2 _x1 _x2 _x3 (alice_sends_message_1_to_server_4 ? ? ? ?) ? ?); Assumption.
Qed.

Remark rem_4 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_3 _x1 _x2 _x3 alice_sends_message_1_to_server_11 ? ? ?); Assumption.
Qed.

Remark rem_5 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_27 nil).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_25 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_6 : (EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_27 nil).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_5 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_7 : (_x1:term)(__aux_7 _x1) -> (EX _x:term | (__aux_7 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_8 : (EX _x:term | (__aux_7 _x)).
Proof.
   Intros.
  Refine (rem_7 alice alice_sends_message_1_to_server_1); Assumption.
Qed.

Remark rem_9 : (EX _x:term | (__aux_7 _x)).
Proof.
   Intros.
  Refine (rem_8); Assumption.
Qed.

Remark rem_10 : (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_27 nil).
Proof.
   Intros. Refine (rem_6 rem_9 ? ?); Assumption.
Qed.

Remark rem_11 : (_x1:term)(__aux_9 _x1) -> (EX _x:term | (__aux_9 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_12 : (EX _x:term | (__aux_9 _x)).
Proof.
   Intros.
  Refine (rem_11 bob alice_sends_message_1_to_server_3); Assumption.
Qed.

Remark rem_13 : (EX _x:term | (__aux_9 _x)).
Proof.
   Intros.
  Refine (rem_12); Assumption.
Qed.

Remark rem_14 : (EX _x:term | (__aux_11 _x)) -> (__aux_27 nil).
Proof.
   Intros. Refine (rem_10 rem_13 ?); Assumption.
Qed.

Remark rem_15 : (_x1:term)(__aux_11 _x1) -> (EX _x:term | (__aux_11 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_16 : (_x1:term)(__aux_13 _x1) -> (EX _x:term | (__aux_11 _x)).
Proof.
  Intros _x1. Intros.
  Refine (rem_15 (noncea _x1) (alice_sends_message_1_to_server_5 _x1 ?)); Assumption.
Qed.

Remark rem_17 : (_x1:term)(__aux_13 _x1) -> (EX _x:term | (__aux_11 _x)).
Proof.
  Intros _x1. Intros.
  Refine (rem_16 _x1 ?); Assumption.
Qed.

Remark rem_18 : (EX _x:term | (__aux_13 _x)) -> (EX _x:term | (__aux_11 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intros. Apply (rem_17 _x1); Tauto.
Qed.

Remark rem_19 : (_x1:term)(__aux_13 _x1) -> (EX _x:term | (__aux_13 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_20 : (_x1:term)(_x2:term)(__aux_14 _x2) -> (__aux_7 _x1) -> (EX _x:term | (__aux_13 _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_19 (cons _x1 _x2) (alice_sends_message_1_to_server_6 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_21 : (EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_14 _x)) -> (EX _x:term | (__aux_13 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_20 _x1 _x2); Tauto.
Qed.

Remark rem_22 : (EX _x:term | (__aux_14 _x)) -> (EX _x:term | (__aux_13 _x)).
Proof.
   Intros. Refine (rem_21 rem_9 ?); Assumption.
Qed.

Remark rem_23 : (_x1:term)(__aux_14 _x1) -> (EX _x:term | (__aux_14 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_24 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_9 _x1) -> (EX _x:term | (__aux_14 _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_23 (cons _x1 _x2) (alice_sends_message_1_to_server_8 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_25 : (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_12 _x)) -> (EX _x:term | (__aux_14 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_24 _x1 _x2); Tauto.
Qed.

Remark rem_26 : (EX _x:term | (__aux_12 _x)) -> (EX _x:term | (__aux_14 _x)).
Proof.
   Intros. Refine (rem_25 rem_13 ?); Assumption.
Qed.

Remark rem_27 : (_x1:term)(__aux_12 _x1) -> (EX _x:term | (__aux_12 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_28 : (EX _x:term | (__aux_12 _x)).
Proof.
   Intros.
  Refine (rem_27 nil alice_sends_message_1_to_server_11); Assumption.
Qed.

Remark rem_29 : (EX _x:term | (__aux_12 _x)).
Proof.
   Intros.
  Refine (rem_28); Assumption.
Qed.

Remark rem_30 : (EX _x:term | (__aux_14 _x)).
Proof.
   Intros. Refine (rem_26 rem_29); Assumption.
Qed.

Remark rem_31 : (EX _x:term | (__aux_13 _x)).
Proof.
   Intros. Refine (rem_22 rem_30); Assumption.
Qed.

Remark rem_32 : (EX _x:term | (__aux_11 _x)).
Proof.
   Intros. Refine (rem_18 rem_31); Assumption.
Qed.

Remark rem_33 : (__aux_27 nil).
Proof.
   Intros. Refine (rem_14 rem_32); Assumption.
Qed.

Remark rem_34 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_34 server).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_23 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_35 : (EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_34 server).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_34 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_36 : (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_34 server).
Proof.
   Intros. Refine (rem_35 rem_9 ? ?); Assumption.
Qed.

Remark rem_37 : (EX _x:term | (__aux_11 _x)) -> (__aux_34 server).
Proof.
   Intros. Refine (rem_36 rem_13 ?); Assumption.
Qed.

Remark rem_38 : (__aux_34 server).
Proof.
   Intros. Refine (rem_37 rem_32); Assumption.
Qed.

Remark rem_39 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_24 sym).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_19 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_40 : (EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_24 sym).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_39 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_41 : (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_24 sym).
Proof.
   Intros. Refine (rem_40 rem_9 ? ?); Assumption.
Qed.

Remark rem_42 : (EX _x:term | (__aux_11 _x)) -> (__aux_24 sym).
Proof.
   Intros. Refine (rem_41 rem_13 ?); Assumption.
Qed.

Remark rem_43 : (__aux_24 sym).
Proof.
   Intros. Refine (rem_42 rem_32); Assumption.
Qed.

Remark rem_44 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_7 _x2) -> (__aux_9 _x1) -> (__aux_20 _x1).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_4 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_45 : (_x1:term)(EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_9 _x1) -> (__aux_20 _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_44 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_46 : (_x1:term)(EX _x:term | (__aux_11 _x)) -> (__aux_9 _x1) -> (__aux_20 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_45 _x1 rem_9 ? ?); Assumption.
Qed.

Remark rem_47 : (_x1:term)(__aux_9 _x1) -> (__aux_20 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_46 _x1 rem_32 ?); Assumption.
Qed.

Remark rem_48 : (__aux_20 bob).
Proof.
   Intros.
  Refine (rem_47 bob alice_sends_message_1_to_server_3); Assumption.
Qed.

Remark rem_49 : (__aux_20 bob).
Proof.
   Intros.
  Refine (rem_48); Assumption.
Qed.

Remark rem_50 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_31 _x1).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_16 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_51 : (_x1:term)(EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (__aux_7 _x1) -> (__aux_31 _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_50 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_52 : (_x1:term)(EX _x:term | (__aux_11 _x)) -> (__aux_7 _x1) -> (__aux_31 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_51 _x1 rem_13 ? ?); Assumption.
Qed.

Remark rem_53 : (_x1:term)(__aux_7 _x1) -> (__aux_31 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_52 _x1 rem_32 ?); Assumption.
Qed.

Remark rem_54 : (__aux_31 alice).
Proof.
   Intros.
  Refine (rem_53 alice alice_sends_message_1_to_server_1); Assumption.
Qed.

Remark rem_55 : (__aux_31 alice).
Proof.
   Intros.
  Refine (rem_54); Assumption.
Qed.

Remark rem_56 : (_x1:term)(_x2:term)(_x3:term)(__aux_9 _x3) -> (__aux_7 _x2) -> (__aux_11 _x1) -> (__aux_18 _x1).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_2 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_57 : (_x1:term)(EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_9 _x)) -> (__aux_11 _x1) -> (__aux_18 _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_56 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_58 : (_x1:term)(EX _x:term | (__aux_9 _x)) -> (__aux_11 _x1) -> (__aux_18 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_57 _x1 rem_9 ? ?); Assumption.
Qed.

Remark rem_59 : (_x1:term)(__aux_11 _x1) -> (__aux_18 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_58 _x1 rem_13 ?); Assumption.
Qed.

Remark rem_60 : (_x1:term)(__aux_13 _x1) -> (__aux_18 (noncea _x1)).
Proof.
  Intros _x1. Intros.
  Refine (rem_59 (noncea _x1) (alice_sends_message_1_to_server_5 _x1 ?)); Assumption.
Qed.

Remark rem_61 : (_x1:term)(__aux_13 _x1) -> (__aux_18 (noncea _x1)).
Proof.
  Intros _x1. Intros.
  Refine (rem_60 _x1 ?); Assumption.
Qed.

Remark rem_62 : (_x1:term)(_x2:term)(__aux_17 (key sym (cons alice (cons server nil)))) -> (__aux_36 (cons (noncea (cons alice (cons bob nil))) (cons bob (cons _x1 (cons _x2 nil))))) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (alice_gets_server_message_and_forwards_submessage_to_bob_1 _x1 _x2 (intruder_knows_previous_server_messages ? ? ? ?)); Assumption.
Qed.

Remark rem_63 : (_x1:term)(_x2:term)(__aux_24 sym) -> (__aux_37 (cons bob (cons _x1 (cons _x2 nil)))) -> (__aux_35 (cons alice (cons server nil))) -> (__aux_18 (noncea (cons alice (cons bob nil)))) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_62 _x1 _x2 (server_answers_A_with_encrypted_packet_26 ? ? ? ?) (intruder_knows_previous_server_messages_1 ? ? ? ?)); Assumption.
Qed.

Remark rem_64 : (_x1:term)(_x2:term)(__aux_31 alice) -> (__aux_20 bob) -> (__aux_38 (cons _x1 (cons _x2 nil))) -> (__aux_33 (cons server nil)) -> (__aux_13 (cons alice (cons bob nil))) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_63 _x1 _x2 rem_43 (intruder_knows_previous_server_messages_3 ? ? ? ?) (server_answers_A_with_encrypted_packet_28 ? ? ? ?) (rem_61 ? ?)); Assumption.
Qed.

Remark rem_65 : (_x1:term)(_x2:term)(__aux_7 alice) -> (__aux_34 server) -> (__aux_27 nil) -> (__aux_40 (cons _x2 nil)) -> (__aux_14 (cons bob nil)) -> (__aux_39 _x1) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_64 _x1 _x2 rem_55 rem_49 (intruder_knows_previous_server_messages_5 ? ? ? ?) (server_answers_A_with_encrypted_packet_30 ? ? ? ?) (alice_sends_message_1_to_server_6 ? ? ? ?)); Assumption.
Qed.

Remark rem_66 : (_x1:term)(_x2:term)(__aux_9 bob) -> (__aux_27 nil) -> (__aux_12 nil) -> (__aux_42 _x2) -> (__aux_39 _x1) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_65 _x1 _x2 alice_sends_message_1_to_server_1 rem_38 rem_33 (intruder_knows_previous_server_messages_9 ? ? ? ?) (alice_sends_message_1_to_server_8 ? ? ? ?) ?); Assumption.
Qed.

Remark rem_67 : (_x1:term)(_x2:term)(__aux_42 _x2) -> (__aux_39 _x1) -> (__aux_44 (__aux__vars8 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_66 _x1 _x2 alice_sends_message_1_to_server_3 rem_33 alice_sends_message_1_to_server_11 ? ?); Assumption.
Qed.

Remark rem_68 : (_x1:term)(_x2:term)(__aux_39 _x2) -> (__aux_42 _x1) -> (knows _x1).
Proof.
  Intros _x1 _x2. Intros.
  Refine (alice_gets_server_message_and_forwards_submessage_to_bob _x1 _x2 (rem_67 ? ? ? ?)); Assumption.
Qed.

Remark rem_69 : (_x1:term)(EX _x:term | (__aux_39 _x)) -> (__aux_42 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_68 _x1 _x2); Tauto.
Qed.

Remark rem_70 : (_x1:term)(__aux_39 _x1) -> (EX _x:term | (__aux_39 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_71 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (EX _x:term | (__aux_39 _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_70 (key _x1 _x2) (intruder_knows_previous_server_messages_12 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_72 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (EX _x:term | (__aux_39 _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_71 _x1 _x2 ? ?); Assumption.
Qed.

Remark rem_73 : (EX _x:term | (__aux_41 _x)) -> (EX _x:term | (__aux_24 _x)) -> (EX _x:term | (__aux_39 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intros. Apply (rem_72 _x1 _x2); Tauto.
Qed.

Remark rem_74 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (__aux_41 (old_session _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (intruder_knows_previous_server_messages_8 _x1 _x2 _x3 (rem_4 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_75 : (_x1:term)(__aux_41 _x1) -> (EX _x:term | (__aux_41 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_76 : (_x1:term)(_x2:term)(_x3:term)(__aux_11 _x3) -> (__aux_9 _x2) -> (__aux_7 _x1) -> (EX _x:term | (__aux_41 _x)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_75 (old_session _x1 _x2 _x3) (rem_74 _x1 _x2 _x3 ? ? ?)); Assumption.
Qed.

Remark rem_77 : (EX _x:term | (__aux_7 _x)) -> (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (EX _x:term | (__aux_41 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_76 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_78 : (EX _x:term | (__aux_9 _x)) -> (EX _x:term | (__aux_11 _x)) -> (EX _x:term | (__aux_41 _x)).
Proof.
   Intros. Refine (rem_77 rem_9 ? ?); Assumption.
Qed.

Remark rem_79 : (EX _x:term | (__aux_11 _x)) -> (EX _x:term | (__aux_41 _x)).
Proof.
   Intros. Refine (rem_78 rem_13 ?); Assumption.
Qed.

Remark rem_80 : (EX _x:term | (__aux_41 _x)).
Proof.
   Intros. Refine (rem_79 rem_32); Assumption.
Qed.

Remark rem_81 : (EX _x:term | (__aux_24 _x)) -> (EX _x:term | (__aux_39 _x)).
Proof.
   Intros. Refine (rem_73 rem_80 ?); Assumption.
Qed.

Remark rem_82 : (_x1:term)(__aux_24 _x1) -> (EX _x:term | (__aux_24 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_83 : (EX _x:term | (__aux_24 _x)).
Proof.
   Intros.
  Refine (rem_82 sym rem_43); Assumption.
Qed.

Remark rem_84 : (EX _x:term | (__aux_39 _x)).
Proof.
   Intros. Refine (rem_81 rem_83); Assumption.
Qed.

Remark rem_85 : (_x1:term)(__aux_42 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intros. Refine (rem_69 _x1 rem_84 ?); Assumption.
Qed.

Remark rem_86 : (_x1:term)(_x2:term)(__aux_29 _x2) -> (__aux_43 _x1) -> (knows (crypt _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_85 (crypt _x1 _x2) (intruder_knows_previous_server_messages_10 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_87 : (_x1:term)(_x2:term)(__aux_29 _x2) -> (__aux_43 _x1) -> (knows (crypt _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_86 _x1 _x2 ? ?); Assumption.
Qed.

Remark rem_88 : (_x1:term)(_x2:term)(_x3:term)(__aux_43 (cons _x2 (cons _x1 nil))) -> (__aux_29 (key sym (cons _x3 (cons server nil)))) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_3 _x1 _x2 _x3 (rem_87 ? ? ? ?)); Assumption.
Qed.

Remark rem_89 : (_x1:term)(_x2:term)(_x3:term)(__aux_24 sym) -> (__aux_30 (cons _x1 nil)) -> (__aux_32 (cons _x3 (cons server nil))) -> (__aux_39 _x2) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_88 _x1 _x2 _x3 (intruder_knows_previous_server_messages_11 ? ? ? ?) (server_answers_A_with_encrypted_packet_18 ? ? ? ?)); Assumption.
Qed.

Remark rem_90 : (_x1:term)(_x2:term)(_x3:term)(__aux_27 nil) -> (__aux_33 (cons server nil)) -> (__aux_20 _x3) -> (__aux_39 _x2) -> (__aux_31 _x1) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_89 _x1 _x2 _x3 rem_43 (server_answers_A_with_encrypted_packet_15 ? ? ? ?) (server_answers_A_with_encrypted_packet_20 ? ? ? ?) ?); Assumption.
Qed.

Remark rem_91 : (_x1:term)(_x2:term)(_x3:term)(__aux_34 server) -> (__aux_27 nil) -> (__aux_20 _x3) -> (__aux_39 _x2) -> (__aux_31 _x1) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_90 _x1 _x2 _x3 rem_33 (server_answers_A_with_encrypted_packet_30 ? ? ? ?) ? ? ?); Assumption.
Qed.

Remark rem_92 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_39 _x2) -> (__aux_31 _x1) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_91 _x1 _x2 _x3 rem_38 rem_33 ? ? ?); Assumption.
Qed.

Remark rem_93 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_31 _x2) -> (__aux_39 _x1) -> (__aux_49 (nonceb _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_1 _x1 _x2 _x3 (rem_92 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_94 : (_x1:term)(__aux_58 sym) -> (__aux_59 _x1) -> (__aux_5 (__aux__vars5 _x1)).
Proof.
  Intros _x1. Intros.
  Refine (intruder_can_decrypt_if_has_symmetric_key_2 _x1 (intruder_knows_all_previous_session_keys ? ? ? ?)); Assumption.
Qed.

Remark rem_95 : (_x1:term)(__aux_59 _x1) -> (__aux_5 (__aux__vars5 _x1)).
Proof.
  Intros _x1. Intros.
  Refine (rem_94 _x1 intruder_knows_all_previous_session_keys_1 ?); Assumption.
Qed.

Remark rem_96 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_31 _x2) -> (__aux_39 _x1) -> (__aux_50 _x1).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_2 _x1 _x2 _x3 (rem_92 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_97 : (_x1:term)(EX _x:term | (__aux_31 _x)) -> (EX _x:term | (__aux_20 _x)) -> (__aux_39 _x1) -> (__aux_50 _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_96 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_98 : (_x1:term)(__aux_31 _x1) -> (EX _x:term | (__aux_31 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_99 : (EX _x:term | (__aux_31 _x)).
Proof.
   Intros.
  Refine (rem_98 alice rem_55); Assumption.
Qed.

Remark rem_100 : (_x1:term)(EX _x:term | (__aux_20 _x)) -> (__aux_39 _x1) -> (__aux_50 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_97 _x1 rem_99 ? ?); Assumption.
Qed.

Remark rem_101 : (_x1:term)(__aux_20 _x1) -> (EX _x:term | (__aux_20 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_102 : (EX _x:term | (__aux_20 _x)).
Proof.
   Intros.
  Refine (rem_101 bob rem_49); Assumption.
Qed.

Remark rem_103 : (_x1:term)(__aux_39 _x1) -> (__aux_50 _x1).
Proof.
  Intros _x1. Intros. Refine (rem_100 _x1 rem_102 ?); Assumption.
Qed.

Remark rem_104 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (__aux_50 (key _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_103 (key _x1 _x2) (intruder_knows_previous_server_messages_12 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_105 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (__aux_50 (key _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_104 _x1 _x2 ? ?); Assumption.
Qed.

Remark rem_106 : (_x1:term)(_x2:term)(__aux_50 (key sym _x2)) -> (__aux_49 _x1) -> (__aux_6 (__aux__vars6 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (intruder_can_decrypt_if_has_symmetric_key_1 _x1 _x2 (agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge ? ? ? ?)); Assumption.
Qed.

Remark rem_107 : (_x1:term)(_x2:term)(__aux_24 sym) -> (__aux_41 _x2) -> (__aux_49 _x1) -> (__aux_6 (__aux__vars6 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_106 _x1 _x2 (rem_105 ? ? ? ?) ?); Assumption.
Qed.

Remark rem_108 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_49 _x1) -> (__aux_6 (__aux__vars6 _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_107 _x1 _x2 rem_43 ? ?); Assumption.
Qed.

Remark rem_109 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_59 _x2) -> (__aux_49 _x1) -> (knows _x1).
Proof.
  Intros _x1 _x2. Intros.
  Refine (intruder_can_decrypt_if_has_symmetric_key _x1 _x2 (rem_108 ? ? ? ?) (rem_95 ? ?)); Assumption.
Qed.

Remark rem_110 : (_x1:term)(EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)) -> (__aux_49 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_109 _x1 _x2); Tauto.
Qed.

Remark rem_111 : (_x1:term)(_x2:term)(_x3:term)(knows (cons _x2 (cons _x3 nil))) -> (knows _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (server_answers_A_with_encrypted_packet_33 _x1 _x2 _x3 (intruder_can_build_pairs ? ? ? ?)); Assumption.
Qed.

Remark rem_112 : (_x1:term)(_x2:term)(_x3:term)(knows (cons _x3 nil)) -> (knows _x2) -> (knows _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_111 _x1 _x2 _x3 (intruder_can_build_pairs ? ? ? ?) ?); Assumption.
Qed.

Remark rem_113 : (_x1:term)(_x2:term)(_x3:term)(knows nil) -> (knows _x3) -> (knows _x2) -> (knows _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_112 _x1 _x2 _x3 (intruder_can_build_pairs ? ? ? ?) ? ?); Assumption.
Qed.

Remark rem_114 : (_x1:term)(_x2:term)(_x3:term)(knows _x3) -> (knows _x2) -> (knows _x1) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_113 _x1 _x2 _x3 intruder_knows_nil ? ? ?); Assumption.
Qed.

Remark rem_115 : (_x1:term)(_x2:term)(_x3:term)(knows _x3) -> (knows _x2) -> (knows _x1) -> (__aux_41 (old_session _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (intruder_knows_previous_server_messages_8 _x1 _x2 _x3 (rem_114 ? ? ? ? ? ?)); Assumption.
Qed.

Remark rem_116 : (_x1:term)(__aux_41 _x1) -> (__aux_59 _x1) -> (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_117 : (_x1:term)(_x2:term)(_x3:term)(__aux_59 (old_session _x1 _x2 _x3)) -> (knows _x3) -> (knows _x2) -> (knows _x1) -> (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_116 (old_session _x1 _x2 _x3) (rem_115 _x1 _x2 _x3 ? ? ?) ?); Assumption.
Qed.

Remark rem_118 : (_x1:term)(_x2:term)(_x3:term)(knows _x3) -> (knows _x2) -> (knows _x1) -> (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_117 _x1 _x2 _x3 (intruder_knows_all_previous_session_keys_2 ? ? ?) ? ? ?); Assumption.
Qed.

Remark rem_119 : (EX _x:term | (knows _x)) -> (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intros. Apply (rem_118 _x1 _x1 _x1); Tauto.
Qed.

Remark rem_120 : (_x1:term)(_x2:term)(__aux_7 _x2) -> (__aux_8 _x1) -> (knows _x1).
Proof.
  Intros _x1 _x2. Intros.
  Refine (intruder_can_take_second_components _x1 _x2 (alice_sends_message_1_to_server ? ? ? ?)); Assumption.
Qed.

Remark rem_121 : (_x1:term)(EX _x:term | (__aux_7 _x)) -> (__aux_8 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_120 _x1 _x2); Tauto.
Qed.

Remark rem_122 : (_x1:term)(__aux_8 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intros. Refine (rem_121 _x1 rem_9 ?); Assumption.
Qed.

Remark rem_123 : (_x1:term)(_x2:term)(__aux_10 _x2) -> (__aux_9 _x1) -> (knows (cons _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_122 (cons _x1 _x2) (alice_sends_message_1_to_server_2 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_124 : (_x1:term)(_x2:term)(__aux_10 _x2) -> (__aux_9 _x1) -> (knows (cons _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_123 _x1 _x2 ? ?); Assumption.
Qed.

Remark rem_125 : (_x1:term)(_x2:term)(__aux_9 _x2) -> (__aux_10 _x1) -> (knows _x1).
Proof.
  Intros _x1 _x2. Intros.
  Refine (intruder_can_take_second_components _x1 _x2 (rem_124 ? ? ? ?)); Assumption.
Qed.

Remark rem_126 : (_x1:term)(EX _x:term | (__aux_9 _x)) -> (__aux_10 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_125 _x1 _x2); Tauto.
Qed.

Remark rem_127 : (_x1:term)(__aux_10 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intros. Refine (rem_126 _x1 rem_13 ?); Assumption.
Qed.

Remark rem_128 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_11 _x1) -> (knows (cons _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_127 (cons _x1 _x2) (alice_sends_message_1_to_server_4 _x1 _x2 ? ?)); Assumption.
Qed.

Remark rem_129 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_11 _x1) -> (knows (cons _x1 _x2)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_128 _x1 _x2 ? ?); Assumption.
Qed.

Remark rem_130 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_11 _x1) -> (knows _x1).
Proof.
  Intros _x1 _x2. Intros.
  Refine (intruder_can_take_first_components _x1 _x2 (rem_129 ? ? ? ?)); Assumption.
Qed.

Remark rem_131 : (_x1:term)(EX _x:term | (__aux_12 _x)) -> (__aux_11 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_130 _x1 _x2); Tauto.
Qed.

Remark rem_132 : (_x1:term)(__aux_11 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intros. Refine (rem_131 _x1 rem_29 ?); Assumption.
Qed.

Remark rem_133 : (_x1:term)(__aux_13 _x1) -> (knows (noncea _x1)).
Proof.
  Intros _x1. Intros.
  Refine (rem_132 (noncea _x1) (alice_sends_message_1_to_server_5 _x1 ?)); Assumption.
Qed.

Remark rem_134 : (_x1:term)(__aux_13 _x1) -> (knows (noncea _x1)).
Proof.
  Intros _x1. Intros.
  Refine (rem_133 _x1 ?); Assumption.
Qed.

Remark rem_135 : (_x1:term)(knows _x1) -> (EX _x:term | (knows _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_136 : (_x1:term)(__aux_13 _x1) -> (EX _x:term | (knows _x)).
Proof.
  Intros _x1. Intros.
  Refine (rem_135 (noncea _x1) (rem_134 _x1 ?)); Assumption.
Qed.

Remark rem_137 : (_x1:term)(__aux_13 _x1) -> (EX _x:term | (knows _x)).
Proof.
  Intros _x1. Intros.
  Refine (rem_136 _x1 ?); Assumption.
Qed.

Remark rem_138 : (EX _x:term | (__aux_13 _x)) -> (EX _x:term | (knows _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intros. Apply (rem_137 _x1); Tauto.
Qed.

Remark rem_139 : (EX _x:term | (knows _x)).
Proof.
   Intros. Refine (rem_138 rem_31); Assumption.
Qed.

Remark rem_140 : (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)).
Proof.
   Intros. Refine (rem_119 rem_139); Assumption.
Qed.

Remark rem_141 : (_x1:term)(__aux_49 _x1) -> (knows _x1).
Proof.
  Intros _x1. Intros. Refine (rem_110 _x1 rem_140 ?); Assumption.
Qed.

Remark rem_142 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_31 _x2) -> (__aux_39 _x1) -> (knows (nonceb _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_141 (nonceb _x1 _x2 _x3) (rem_93 _x1 _x2 _x3 ? ? ?)); Assumption.
Qed.

Remark rem_143 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_31 _x2) -> (__aux_39 _x1) -> (knows (nonceb _x1 _x2 _x3)).
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_142 _x1 _x2 _x3 ? ? ?); Assumption.
Qed.

Remark rem_144 : (_x1:term)(_x2:term)(_x3:term)(knows (s (nonceb _x1 _x2 _x3))) -> (knows _x1) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (intruder_knows_session_key_as_seen_by_B _x1 _x2 _x3 (intruder_can_encrypt ? ? ? ?) ?); Assumption.
Qed.

Remark rem_145 : (_x1:term)(_x2:term)(_x3:term)(knows (nonceb _x1 _x2 _x3)) -> (knows _x1) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_144 _x1 _x2 _x3 (intruder_can_compute_successors ? ?) ?); Assumption.
Qed.

Remark rem_146 : (_x1:term)(_x2:term)(_x3:term)(__aux_20 _x3) -> (__aux_31 _x2) -> (__aux_39 _x1) -> (knows _x1) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
  Intros _x1 _x2 _x3. Intros.
  Refine (rem_145 _x1 _x2 _x3 (rem_143 ? ? ? ? ? ?) ?); Assumption.
Qed.

Remark rem_147 : (EX _x:term | (__aux_31 _x)) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)) -> (EX _x:term | (__aux_20 _x)) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x3; Intro.
   Intros. Apply (rem_146 _x1 _x2 _x3); Tauto.
Qed.

Remark rem_148 : (EX _x:term | (__aux_39 _x) /\ (knows _x)) -> (EX _x:term | (__aux_20 _x)) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
   Intros. Refine (rem_147 rem_99 ? ?); Assumption.
Qed.

Remark rem_149 : (EX _x:term | (__aux_39 _x) /\ (knows _x)) -> reach_intruder_knows_session_key_as_seen_by_B.
Proof.
   Intros. Refine (rem_148 ? rem_102); Assumption.
Qed.

Remark rem_150 : (_x1:term)(__aux_39 _x1) -> (knows _x1) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_151 : (_x1:term)(_x2:term)(knows (key _x1 _x2)) -> (__aux_41 _x2) -> (__aux_24 _x1) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_150 (key _x1 _x2) (intruder_knows_previous_server_messages_12 _x1 _x2 ? ?) ?); Assumption.
Qed.

Remark rem_152 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_59 _x2) -> (__aux_24 _x1) -> (__aux_58 _x1) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
  Intros _x1 _x2. Intros.
  Refine (rem_151 _x1 _x2 (intruder_knows_all_previous_session_keys ? ? ? ?) ? ?); Assumption.
Qed.

Remark rem_153 : (EX _x:term | (__aux_24 _x) /\ (__aux_58 _x)) -> (EX _x:term | (__aux_41 _x) /\ (__aux_59 _x)) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
   Intro hyp; Elim hyp; Clear hyp; Intro _x1; Intro.
   Intro hyp; Elim hyp; Clear hyp; Intro _x2; Intro.
   Intros. Apply (rem_152 _x1 _x2); Tauto.
Qed.

Remark rem_154 : (EX _x:term | (__aux_24 _x) /\ (__aux_58 _x)) -> (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
   Intros. Refine (rem_153 ? rem_140); Assumption.
Qed.

Remark rem_155 : (_x1:term)(__aux_24 _x1) -> (__aux_58 _x1) -> (EX _x:term | (__aux_24 _x) /\ (__aux_58 _x)).
Proof.
  Intro Z. Intros. Exists Z; Tauto.
Qed.

Remark rem_156 : (__aux_58 sym) -> (EX _x:term | (__aux_24 _x) /\ (__aux_58 _x)).
Proof.
   Intros.
  Refine (rem_155 sym rem_43 ?); Assumption.
Qed.

Remark rem_157 : (EX _x:term | (__aux_24 _x) /\ (__aux_58 _x)).
Proof.
   Intros.
  Refine (rem_156 intruder_knows_all_previous_session_keys_1); Assumption.
Qed.

Remark rem_158 : (EX _x:term | (__aux_39 _x) /\ (knows _x)).
Proof.
   Intros. Refine (rem_154 rem_157); Assumption.
Qed.

Remark rem_159 : reach_intruder_knows_session_key_as_seen_by_B.
Proof.
   Intros. Refine (rem_149 rem_158); Assumption.
Qed.

Theorem thm_intruder_knows_session_key_as_seen_by_B : reach_intruder_knows_session_key_as_seen_by_B.
Proof rem_159.
