(* [sigd] Signature definition. *)

Inductive term : Set :=
    alice : term
  | bob : term
  | cons : term -> term -> term
  | crypt : term -> term -> term
  | f1 : term -> term -> term -> term
  | f2 : term -> term -> term
  | f3 : term -> term -> term
  | f4 : term -> term -> term
  | f5 : term -> term -> term
  | h : term -> term
  | i : term
  | key : term -> term -> term
  | nai : term -> term
  | nil : term
  | nonces_current : term -> term -> term -> term
  | nonces_old : term -> term -> term -> term
  | prv : term
  | pub : term
  | request_id : term
  | respond_id : term
  | s : term -> term
  | server : term
  | session_current : term -> term -> term -> term
  | session_old : term -> term -> term -> term
  | success : term
  | sym : term
.

(* [modd] Model definition. *)

Inductive auto___type_21 : term -> Prop :=
    trans___type_21_1 : forall X:term, auto___type_21 X
with auto___type_20 : term -> Prop :=
    trans___type_20_1 : forall X:term, auto___type_20 X
with auto___type_19 : term -> Prop :=
    trans___type_19_1 : forall X:term, auto___type_19 X
with auto___type_2 : term -> Prop :=
    trans___type_2_s_1 : forall X1:term, auto_knows_old X1 -> auto___type_2 (s X1)
  | trans___type_2_nil_1 : auto___type_2 nil
  | trans___type_2_h_1 : forall X1:term, auto___def_44 X1 -> auto___type_2 (h X1)
  | trans___type_2_h_2 : forall X1:term, auto___def_26 X1 -> auto___type_2 (h X1)
  | trans___type_2_h_3 : forall X1:term, auto_knows_old X1 -> auto___type_2 (h X1)
  | trans___type_2_respond_id_1 : auto___type_2 respond_id
  | trans___type_2_f2_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___type_2 (f2 X1 X2)
  | trans___type_2_success_1 : auto___type_2 success
  | trans___type_2_request_id_1 : auto___type_2 request_id
  | trans___type_2_crypt_1 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___type_2 (crypt X1 X2)
  | trans___type_2_crypt_2 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___type_2 (crypt X1 X2)
  | trans___type_2_nai_1 : forall X1:term, auto_agent X1 -> auto___type_2 (nai X1)
  | trans___type_2_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_2 (nonces_old X1 X2 X3)
  | trans___type_2_cons_1 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___type_2 (cons X1 X2)
  | trans___type_2_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___type_2 (f1 X1 X2 X3)
with auto___def_32 : term -> Prop :=
    trans___def_32_cons_1 : forall X1 X2:term, auto___def_33 X1 -> auto___def_24 X2 -> auto___def_32 (cons X1 X2)
with auto___def_66 : term -> Prop :=
    trans___def_66_sym_1 : auto___def_66 sym
with auto___def_96 : term -> Prop :=
    trans___def_96_f4_1 : forall X1 X2:term, auto___def_87 X1 -> auto___def_79 X2 -> auto___def_96 (f4 X1 X2)
with auto___def_94 : term -> Prop :=
    trans___def_94_cons_1 : forall X1 X2:term, auto___type_12 X1 -> auto___def_95 X2 -> auto___def_94 (cons X1 X2)
with auto___def_134 : term -> Prop :=
    trans___def_134_nil_1 : auto___def_134 nil
with auto___def_31 : term -> Prop :=
    trans___def_31_f4_1 : forall X1 X2:term, auto___def_18 X1 -> auto___def_10 X2 -> auto___def_31 (f4 X1 X2)
with auto___def_9 : term -> Prop :=
    trans___def_9_s_1 : forall X1:term, auto_knows_old X1 -> auto___def_9 (s X1)
  | trans___def_9_nil_1 : auto___def_9 nil
  | trans___def_9_h_1 : forall X1:term, auto___def_44 X1 -> auto___def_9 (h X1)
  | trans___def_9_h_2 : forall X1:term, auto___def_26 X1 -> auto___def_9 (h X1)
  | trans___def_9_h_3 : forall X1:term, auto_knows_old X1 -> auto___def_9 (h X1)
  | trans___def_9_respond_id_1 : auto___def_9 respond_id
  | trans___def_9_f2_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___def_9 (f2 X1 X2)
  | trans___def_9_success_1 : auto___def_9 success
  | trans___def_9_request_id_1 : auto___def_9 request_id
  | trans___def_9_crypt_1 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___def_9 (crypt X1 X2)
  | trans___def_9_crypt_2 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___def_9 (crypt X1 X2)
  | trans___def_9_nai_1 : forall X1:term, auto_agent X1 -> auto___def_9 (nai X1)
  | trans___def_9_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_9 (nonces_old X1 X2 X3)
  | trans___def_9_cons_1 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___def_9 (cons X1 X2)
  | trans___def_9_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___def_9 (f1 X1 X2 X3)
with auto___def_30 : term -> Prop :=
    trans___def_30_cons_1 : forall X1 X2:term, auto___def_31 X1 -> auto___def_32 X2 -> auto___def_30 (cons X1 X2)
with auto___def_38 : term -> Prop :=
    trans___def_38_key_1 : forall X1 X2:term, auto___def_39 X1 -> auto___def_40 X2 -> auto___def_38 (key X1 X2)
with auto___def_111 : term -> Prop :=
    trans___def_111_cons_1 : forall X1 X2:term, auto___def_101 X1 -> auto___def_107 X2 -> auto___def_111 (cons X1 X2)
with auto___def_45 : term -> Prop :=
    trans___def_45_h_1 : forall X1:term, auto___def_47 X1 -> auto___def_45 (h X1)
with auto___def_63 : term -> Prop :=
    trans___def_63_f4_1 : forall X1 X2:term, auto___def_65 X1 -> auto___type_10 X2 -> auto___def_63 (f4 X1 X2)
with auto___def_110 : term -> Prop :=
    trans___def_110_h_1 : forall X1:term, auto___def_112 X1 -> auto___def_110 (h X1)
with auto___def_26 : term -> Prop :=
    trans___def_26_cons_1 : forall X1 X2:term, auto___def_27 X1 -> auto___def_28 X2 -> auto___def_26 (cons X1 X2)
with auto___def_60 : term -> Prop :=
    trans___def_60_cons_1 : forall X1 X2:term, auto___type_8 X1 -> auto___def_61 X2 -> auto___def_60 (cons X1 X2)
with auto___def_65 : term -> Prop :=
    trans___def_65_key_1 : forall X1 X2:term, auto___def_66 X1 -> auto___def_67 X2 -> auto___def_65 (key X1 X2)
with auto___type_11 : term -> Prop :=
    trans___type_11_i_1 : auto___type_11 i
  | trans___type_11_bob_1 : auto___type_11 bob
  | trans___type_11_server_1 : auto___type_11 server
  | trans___type_11_alice_1 : auto___type_11 alice
with auto___def_46 : term -> Prop :=
    trans___def_46_cons_1 : forall X1 X2:term, auto___def_36 X1 -> auto___def_42 X2 -> auto___def_46 (cons X1 X2)
with auto___def_7 : term -> Prop :=
    trans___def_7_respond_id_1 : auto___def_7 respond_id
with auto___def_62 : term -> term -> term -> Prop :=
    trans___def_62_1 : forall X1 X2 X3:term, auto___type_1 X1 -> auto_agent X2 -> auto___def_10 X3 -> auto___def_62 X1 X2 X3
with auto___def_40 : term -> Prop :=
    trans___def_40_cons_1 : forall X1 X2:term, auto___type_4 X1 -> auto___def_41 X2 -> auto___def_40 (cons X1 X2)
with auto_peer_keys_current : term -> term -> term -> Prop :=
    trans_peer_keys_current_1 : forall X1 X2 X3:term, auto_peer_keys_current X1 X2 X3
with auto___def_90 : term -> Prop :=
    trans___def_90_h_1 : forall X1:term, auto___def_91 X1 -> auto___def_90 (h X1)
with auto___def_37 : term -> Prop :=
    trans___def_37_cons_1 : forall X1 X2:term, auto___def_43 X1 -> auto___def_42 X2 -> auto___def_37 (cons X1 X2)
with auto___type_9 : term -> Prop :=
    trans___type_9_i_1 : auto___type_9 i
  | trans___type_9_bob_1 : auto___type_9 bob
  | trans___type_9_server_1 : auto___type_9 server
  | trans___type_9_alice_1 : auto___type_9 alice
with auto___def_61 : term -> Prop :=
    trans___def_61_nil_1 : auto___def_61 nil
with auto___def_133 : term -> Prop :=
    trans___def_133_cons_1 : forall X1 X2:term, auto___def_133 (cons X1 X2)
with auto___type_8 : term -> Prop :=
    trans___type_8_i_1 : auto___type_8 i
  | trans___type_8_bob_1 : auto___type_8 bob
  | trans___type_8_server_1 : auto___type_8 server
  | trans___type_8_alice_1 : auto___type_8 alice
with auto___def_49 : term -> Prop :=
    trans___def_49_f4_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___def_49 (f4 X1 X2)
with auto___type_13 : term -> Prop :=
    trans___type_13_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_13 (nonces_current X1 X2 X3)
  | trans___type_13_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_13 (nonces_old X1 X2 X3)
with auto___type_3 : term -> Prop :=
    trans___type_3_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_3 (nonces_old X1 X2 X3)
with auto___def_35 : term -> term -> term -> term -> Prop :=
    trans___def_35_1 : forall X1 X2 X3 X4:term, auto___type_1 X1 -> auto_agent X2 -> auto___type_2 X3 -> auto___def_10 X4 -> auto___def_35 X1 X2 X3 X4
with auto___def_56 : term -> Prop :=
    trans___def_56_key_1 : forall X1 X2:term, auto___def_58 X1 -> auto___def_59 X2 -> auto___def_56 (key X1 X2)
with auto___def_83 : term -> Prop :=
    trans___def_83_crypt_1 : forall X1 X2:term, auto___def_85 X1 -> auto___def_86 X2 -> auto___def_83 (crypt X1 X2)
with auto___def_118 : term -> term -> term -> Prop :=
    trans___def_118_1 : forall X1 X2 X3:term, auto___type_14 X1 -> auto_agent X1 -> auto___type_15 X2 -> auto_agent X2 -> auto_knows_current X3 -> auto___def_118 X1 X2 X3
with auto___def_92 : term -> Prop :=
    trans___def_92_h_1 : forall X1:term, auto___def_94 X1 -> auto___def_92 (h X1)
with auto___def_119 : term -> Prop :=
    trans___def_119_f4_1 : forall X1 X2:term, auto___def_121 X1 -> auto___def_122 X2 -> auto___def_119 (f4 X1 X2)
with auto___def_67 : term -> Prop :=
    trans___def_67_cons_1 : forall X1 X2:term, auto___type_11 X1 -> auto___def_68 X2 -> auto___def_67 (cons X1 X2)
with auto___def_124 : term -> Prop :=
    trans___def_124_cons_1 : forall X1 X2:term, auto___type_17 X1 -> auto___def_125 X2 -> auto___def_124 (cons X1 X2)
with auto___def_117 : term -> term -> term -> Prop :=
    trans___def_117_1 : forall X1 X2 X3:term, auto___type_14 X1 -> auto_agent X1 -> auto___type_15 X2 -> auto_agent X2 -> auto___def_78 X3 -> auto___def_117 X1 X2 X3
with auto___type_14 : term -> Prop :=
    trans___type_14_i_1 : auto___type_14 i
  | trans___type_14_bob_1 : auto___type_14 bob
  | trans___type_14_server_1 : auto___type_14 server
  | trans___type_14_alice_1 : auto___type_14 alice
with auto___def_50 : term -> Prop :=
    trans___def_50_cons_1 : forall X1 X2:term, auto___def_51 X1 -> auto___def_42 X2 -> auto___def_50 (cons X1 X2)
with auto___def_84 : term -> Prop :=
    trans___def_84_cons_1 : forall X1 X2:term, auto___def_88 X1 -> auto___def_89 X2 -> auto___def_84 (cons X1 X2)
with auto___def_29 : term -> Prop :=
    trans___def_29_cons_1 : forall X1 X2:term, auto___type_2 X1 -> auto___def_30 X2 -> auto___def_29 (cons X1 X2)
with auto___def_58 : term -> Prop :=
    trans___def_58_sym_1 : auto___def_58 sym
with auto___type_4 : term -> Prop :=
    trans___type_4_i_1 : auto___type_4 i
  | trans___type_4_bob_1 : auto___type_4 bob
  | trans___type_4_server_1 : auto___type_4 server
  | trans___type_4_alice_1 : auto___type_4 alice
with auto___def_91 : term -> Prop :=
    trans___def_91_cons_1 : forall X1 X2:term, auto___def_92 X1 -> auto___def_93 X2 -> auto___def_91 (cons X1 X2)
with auto___def_127 : term -> term -> term -> Prop :=
    trans___def_127_1 : forall X1 X2 X3:term, auto___def_127 X1 X2 X3
with auto___def_69 : term -> Prop :=
    trans___def_69_nil_1 : auto___def_69 nil
with auto___def_121 : term -> Prop :=
    trans___def_121_key_1 : forall X1 X2:term, auto___def_123 X1 -> auto___def_124 X2 -> auto___def_121 (key X1 X2)
with auto___def_21 : term -> Prop :=
    trans___def_21_cons_1 : forall X1 X2:term, auto_agent X1 -> auto___def_22 X2 -> auto___def_21 (cons X1 X2)
with auto___type_15 : term -> Prop :=
    trans___type_15_i_1 : auto___type_15 i
  | trans___type_15_bob_1 : auto___type_15 bob
  | trans___type_15_server_1 : auto___type_15 server
  | trans___type_15_alice_1 : auto___type_15 alice
with auto___type_10 : term -> Prop :=
    trans___type_10_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_10 (nonces_old X1 X2 X3)
with auto___def_43 : term -> Prop :=
    trans___def_43_h_1 : forall X1:term, auto___def_44 X1 -> auto___def_43 (h X1)
with auto___def_120 : term -> Prop :=
    trans___def_120_f3_1 : forall X1 X2:term, auto___def_121 X1 -> auto___def_122 X2 -> auto___def_120 (f3 X1 X2)
with auto___def_126 : term -> Prop :=
    trans___def_126_nil_1 : auto___def_126 nil
with auto___def_108 : term -> Prop :=
    trans___def_108_h_1 : forall X1:term, auto___def_109 X1 -> auto___def_108 (h X1)
with auto___def_76 : term -> Prop :=
    trans___def_76_respond_id_1 : auto___def_76 respond_id
with auto___def_54 : term -> Prop :=
    trans___def_54_f4_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___def_54 (f4 X1 X2)
with auto___def_130 : term -> Prop :=
    trans___def_130_key_1 : forall X1 X2:term, auto___def_130 (key X1 X2)
with auto___def_16 : term -> Prop :=
    trans___def_16_session_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_16 (session_old X1 X2 X3)
with auto___def_14 : term -> Prop :=
    trans___def_14_crypt_1 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___def_14 (crypt X1 X2)
with auto___def_17 : term -> Prop :=
    trans___def_17_f5_1 : forall X1 X2:term, auto___def_18 X1 -> auto___def_10 X2 -> auto___def_17 (f5 X1 X2)
with auto___def_52 : term -> term -> term -> Prop :=
    trans___def_52_1 : forall X1 X2 X3:term, auto___type_4 X1 -> auto_agent X1 -> auto_agent X2 -> auto___type_5 X2 -> auto___def_9 X3 -> auto___type_6 X3 -> auto___def_52 X1 X2 X3
with auto___def_80 : term -> Prop :=
    trans___def_80_cons_1 : forall X1 X2:term, auto___def_81 X1 -> auto___def_82 X2 -> auto___def_80 (cons X1 X2)
with auto___def_77 : term -> Prop :=
    trans___def_77_nai_1 : forall X1:term, auto_agent X1 -> auto___def_77 (nai X1)
with auto___def_106 : term -> Prop :=
    trans___def_106_cons_1 : forall X1 X2:term, auto___type_15 X1 -> auto___def_107 X2 -> auto___def_106 (cons X1 X2)
with auto___def_131 : term -> Prop :=
    trans___def_131_sym_1 : auto___def_131 sym
with auto___def_82 : term -> Prop :=
    trans___def_82_cons_1 : forall X1 X2:term, auto___def_90 X1 -> auto___def_89 X2 -> auto___def_82 (cons X1 X2)
with auto___def_34 : term -> Prop :=
    trans___def_34_cons_1 : forall X1 X2:term, auto___def_12 X1 -> auto___def_24 X2 -> auto___def_34 (cons X1 X2)
with auto___def_36 : term -> Prop :=
    trans___def_36_f2_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___def_36 (f2 X1 X2)
with auto___def_98 : term -> Prop :=
    trans___def_98_f3_1 : forall X1 X2:term, auto___def_87 X1 -> auto___def_79 X2 -> auto___def_98 (f3 X1 X2)
with auto___def_99 : term -> Prop :=
    trans___def_99_cons_1 : forall X1 X2:term, auto___def_81 X1 -> auto___def_89 X2 -> auto___def_99 (cons X1 X2)
with auto___def_64 : term -> Prop :=
    trans___def_64_f3_1 : forall X1 X2:term, auto___def_65 X1 -> auto___type_10 X2 -> auto___def_64 (f3 X1 X2)
with auto___def_13 : term -> Prop :=
    trans___def_13_cons_1 : forall X1 X2:term, auto___def_25 X1 -> auto___def_24 X2 -> auto___def_13 (cons X1 X2)
with auto___def_53 : term -> term -> term -> Prop :=
    trans___def_53_1 : forall X1 X2 X3:term, auto___type_4 X1 -> auto_agent X1 -> auto_agent X2 -> auto___type_5 X2 -> auto___type_6 X3 -> auto_knows_old X3 -> auto___def_53 X1 X2 X3
with auto_agent : term -> Prop :=
    trans_agent_i_1 : auto_agent i
  | trans_agent_bob_1 : auto_agent bob
  | trans_agent_server_1 : auto_agent server
  | trans_agent_alice_1 : auto_agent alice
with auto___def_59 : term -> Prop :=
    trans___def_59_cons_1 : forall X1 X2:term, auto___type_7 X1 -> auto___def_60 X2 -> auto___def_59 (cons X1 X2)
with auto___def_12 : term -> Prop :=
    trans___def_12_cons_1 : forall X1 X2:term, auto___def_14 X1 -> auto___def_15 X2 -> auto___def_12 (cons X1 X2)
with auto___def_105 : term -> Prop :=
    trans___def_105_cons_1 : forall X1 X2:term, auto___type_14 X1 -> auto___def_106 X2 -> auto___def_105 (cons X1 X2)
with auto___def_104 : term -> Prop :=
    trans___def_104_sym_1 : auto___def_104 sym
with auto___def_101 : term -> Prop :=
    trans___def_101_f2_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___def_101 (f2 X1 X2)
with auto___def_57 : term -> Prop :=
    trans___def_57_nonces_old_1 : forall X1 X2 X3:term, auto___type_6 X1 -> auto_knows_old X1 -> auto___type_4 X2 -> auto_agent X2 -> auto_agent X3 -> auto___type_5 X3 -> auto___def_57 (nonces_old X1 X2 X3)
with auto___def_123 : term -> Prop :=
    trans___def_123_sym_1 : auto___def_123 sym
with auto___type_18 : term -> Prop :=
    trans___type_18_i_1 : auto___type_18 i
  | trans___type_18_bob_1 : auto___type_18 bob
  | trans___type_18_server_1 : auto___type_18 server
  | trans___type_18_alice_1 : auto___type_18 alice
with auto___def_122 : term -> Prop :=
    trans___def_122_nonces_current_1 : forall X1 X2 X3:term, auto_knows_current X1 -> auto___type_14 X2 -> auto_agent X2 -> auto___type_15 X3 -> auto_agent X3 -> auto___def_122 (nonces_current X1 X2 X3)
with auto___def_48 : term -> Prop :=
    trans___def_48_cons_1 : forall X1 X2:term, auto___def_49 X1 -> auto___def_50 X2 -> auto___def_48 (cons X1 X2)
with auto___def_11 : term -> Prop :=
    trans___def_11_cons_1 : forall X1 X2:term, auto___def_12 X1 -> auto___def_13 X2 -> auto___def_11 (cons X1 X2)
with auto___def_109 : term -> Prop :=
    trans___def_109_cons_1 : forall X1 X2:term, auto___def_110 X1 -> auto___def_111 X2 -> auto___def_109 (cons X1 X2)
with auto___type_1 : term -> Prop :=
    trans___type_1_i_1 : auto___type_1 i
  | trans___type_1_bob_1 : auto___type_1 bob
  | trans___type_1_server_1 : auto___type_1 server
  | trans___type_1_alice_1 : auto___type_1 alice
with auto___def_87 : term -> Prop :=
    trans___def_87_key_1 : forall X1 X2:term, auto___def_19 X1 -> auto___def_20 X2 -> auto___def_87 (key X1 X2)
with auto___def_44 : term -> Prop :=
    trans___def_44_cons_1 : forall X1 X2:term, auto___def_45 X1 -> auto___def_46 X2 -> auto___def_44 (cons X1 X2)
with auto___type_12 : term -> Prop :=
    trans___type_12_s_1 : forall X1:term, auto_knows_current X1 -> auto___type_12 (s X1)
  | trans___type_12_nil_1 : auto___type_12 nil
  | trans___type_12_f3_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___type_12 (f3 X1 X2)
  | trans___type_12_h_1 : forall X1:term, auto___def_109 X1 -> auto___type_12 (h X1)
  | trans___type_12_h_2 : forall X1:term, auto___def_91 X1 -> auto___type_12 (h X1)
  | trans___type_12_h_3 : forall X1:term, auto_knows_current X1 -> auto___type_12 (h X1)
  | trans___type_12_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_12 (nonces_current X1 X2 X3)
  | trans___type_12_respond_id_1 : auto___type_12 respond_id
  | trans___type_12_f2_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___type_12 (f2 X1 X2)
  | trans___type_12_success_1 : auto___type_12 success
  | trans___type_12_request_id_1 : auto___type_12 request_id
  | trans___type_12_crypt_1 : forall X1 X2:term, auto___def_85 X1 -> auto___def_86 X2 -> auto___type_12 (crypt X1 X2)
  | trans___type_12_crypt_2 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___type_12 (crypt X1 X2)
  | trans___type_12_crypt_3 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___type_12 (crypt X1 X2)
  | trans___type_12_nai_1 : forall X1:term, auto_agent X1 -> auto___type_12 (nai X1)
  | trans___type_12_f4_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___type_12 (f4 X1 X2)
  | trans___type_12_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_12 (nonces_old X1 X2 X3)
  | trans___type_12_cons_1 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___type_12 (cons X1 X2)
  | trans___type_12_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___type_12 (f1 X1 X2 X3)
  | trans___type_12_f1_2 : forall X1 X2 X3:term, auto___def_87 X1 -> auto___def_85 X2 -> auto___def_79 X3 -> auto___type_12 (f1 X1 X2 X3)
with auto___def_85 : term -> Prop :=
    trans___def_85_session_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_85 (session_current X1 X2 X3)
with auto___def_19 : term -> Prop :=
    trans___def_19_sym_1 : auto___def_19 sym
with auto___def_132 : term -> Prop :=
    trans___def_132_cons_1 : forall X1 X2:term, auto___def_132 (cons X1 X2)
with auto___def_51 : term -> Prop :=
    trans___def_51_f3_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___def_51 (f3 X1 X2)
with auto___def_81 : term -> Prop :=
    trans___def_81_cons_1 : forall X1 X2:term, auto___def_83 X1 -> auto___def_84 X2 -> auto___def_81 (cons X1 X2)
with auto___type_6 : term -> Prop :=
    trans___type_6_s_1 : forall X1:term, auto_knows_old X1 -> auto___type_6 (s X1)
  | trans___type_6_nil_1 : auto___type_6 nil
  | trans___type_6_h_1 : forall X1:term, auto___def_44 X1 -> auto___type_6 (h X1)
  | trans___type_6_h_2 : forall X1:term, auto___def_26 X1 -> auto___type_6 (h X1)
  | trans___type_6_h_3 : forall X1:term, auto_knows_old X1 -> auto___type_6 (h X1)
  | trans___type_6_respond_id_1 : auto___type_6 respond_id
  | trans___type_6_f2_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto___type_6 (f2 X1 X2)
  | trans___type_6_success_1 : auto___type_6 success
  | trans___type_6_request_id_1 : auto___type_6 request_id
  | trans___type_6_crypt_1 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___type_6 (crypt X1 X2)
  | trans___type_6_crypt_2 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___type_6 (crypt X1 X2)
  | trans___type_6_nai_1 : forall X1:term, auto_agent X1 -> auto___type_6 (nai X1)
  | trans___type_6_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_6 (nonces_old X1 X2 X3)
  | trans___type_6_cons_1 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto___type_6 (cons X1 X2)
  | trans___type_6_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___type_6 (f1 X1 X2 X3)
with auto___def_89 : term -> Prop :=
    trans___def_89_nil_1 : auto___def_89 nil
with auto___def_78 : term -> Prop :=
    trans___def_78_s_1 : forall X1:term, auto_knows_current X1 -> auto___def_78 (s X1)
  | trans___def_78_nil_1 : auto___def_78 nil
  | trans___def_78_f3_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___def_78 (f3 X1 X2)
  | trans___def_78_h_1 : forall X1:term, auto___def_109 X1 -> auto___def_78 (h X1)
  | trans___def_78_h_2 : forall X1:term, auto___def_91 X1 -> auto___def_78 (h X1)
  | trans___def_78_h_3 : forall X1:term, auto_knows_current X1 -> auto___def_78 (h X1)
  | trans___def_78_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_78 (nonces_current X1 X2 X3)
  | trans___def_78_respond_id_1 : auto___def_78 respond_id
  | trans___def_78_f2_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___def_78 (f2 X1 X2)
  | trans___def_78_success_1 : auto___def_78 success
  | trans___def_78_request_id_1 : auto___def_78 request_id
  | trans___def_78_crypt_1 : forall X1 X2:term, auto___def_85 X1 -> auto___def_86 X2 -> auto___def_78 (crypt X1 X2)
  | trans___def_78_crypt_2 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___def_78 (crypt X1 X2)
  | trans___def_78_crypt_3 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___def_78 (crypt X1 X2)
  | trans___def_78_nai_1 : forall X1:term, auto_agent X1 -> auto___def_78 (nai X1)
  | trans___def_78_f4_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___def_78 (f4 X1 X2)
  | trans___def_78_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_78 (nonces_old X1 X2 X3)
  | trans___def_78_cons_1 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___def_78 (cons X1 X2)
  | trans___def_78_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___def_78 (f1 X1 X2 X3)
  | trans___def_78_f1_2 : forall X1 X2 X3:term, auto___def_87 X1 -> auto___def_85 X2 -> auto___def_79 X3 -> auto___def_78 (f1 X1 X2 X3)
with auto___def_113 : term -> Prop :=
    trans___def_113_cons_1 : forall X1 X2:term, auto___def_114 X1 -> auto___def_115 X2 -> auto___def_113 (cons X1 X2)
with auto___def_33 : term -> Prop :=
    trans___def_33_f3_1 : forall X1 X2:term, auto___def_18 X1 -> auto___def_10 X2 -> auto___def_33 (f3 X1 X2)
with auto___def_15 : term -> Prop :=
    trans___def_15_cons_1 : forall X1 X2:term, auto___def_23 X1 -> auto___def_24 X2 -> auto___def_15 (cons X1 X2)
with auto___def_129 : term -> Prop :=
    trans___def_129_f3_1 : forall X1 X2:term, auto___def_129 (f3 X1 X2)
with auto_server_keys_current : term -> term -> term -> Prop :=
    trans_server_keys_current_1 : forall X1 X2 X3:term, auto___type_17 X1 -> auto___def_119 X2 -> auto___def_120 X3 -> auto_server_keys_current X1 X2 X3
with auto___def_68 : term -> Prop :=
    trans___def_68_cons_1 : forall X1 X2:term, auto___type_9 X1 -> auto___def_69 X2 -> auto___def_68 (cons X1 X2)
with auto___def_20 : term -> Prop :=
    trans___def_20_cons_1 : forall X1 X2:term, auto___type_1 X1 -> auto___def_21 X2 -> auto___def_20 (cons X1 X2)
with auto___def_125 : term -> Prop :=
    trans___def_125_cons_1 : forall X1 X2:term, auto___type_18 X1 -> auto___def_126 X2 -> auto___def_125 (cons X1 X2)
with auto___def_100 : term -> term -> term -> term -> Prop :=
    trans___def_100_1 : forall X1 X2 X3 X4:term, auto___type_1 X1 -> auto_agent X2 -> auto___type_12 X3 -> auto___def_79 X4 -> auto___def_100 X1 X2 X3 X4
  | trans___def_100_2 : forall X1 X2 X3 X4:term, auto___type_11 X1 -> auto___type_1 X1 -> auto___type_9 X2 -> auto_agent X2 -> auto_knows_current X3 -> auto___type_10 X4 -> auto___def_10 X4 -> auto_knows_current X4 -> auto___def_100 X1 X2 X3 X4
with auto___def_114 : term -> Prop :=
    trans___def_114_f4_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___def_114 (f4 X1 X2)
with auto___def_79 : term -> Prop :=
    trans___def_79_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_79 (nonces_current X1 X2 X3)
with auto___def_115 : term -> Prop :=
    trans___def_115_cons_1 : forall X1 X2:term, auto___def_116 X1 -> auto___def_107 X2 -> auto___def_115 (cons X1 X2)
with auto___def_128 : term -> Prop :=
    trans___def_128_f4_1 : forall X1 X2:term, auto___def_128 (f4 X1 X2)
with auto___def_27 : term -> Prop :=
    trans___def_27_h_1 : forall X1:term, auto___def_29 X1 -> auto___def_27 (h X1)
with auto___def_47 : term -> Prop :=
    trans___def_47_cons_1 : forall X1 X2:term, auto___type_6 X1 -> auto___def_48 X2 -> auto___def_47 (cons X1 X2)
with auto___def_88 : term -> Prop :=
    trans___def_88_f1_1 : forall X1 X2 X3:term, auto___def_87 X1 -> auto___def_85 X2 -> auto___def_79 X3 -> auto___def_88 (f1 X1 X2 X3)
with auto___def_86 : term -> Prop :=
    trans___def_86_f5_1 : forall X1 X2:term, auto___def_87 X1 -> auto___def_79 X2 -> auto___def_86 (f5 X1 X2)
with auto___type_17 : term -> Prop :=
    trans___type_17_i_1 : auto___type_17 i
  | trans___type_17_bob_1 : auto___type_17 bob
  | trans___type_17_server_1 : auto___type_17 server
  | trans___type_17_alice_1 : auto___type_17 alice
with auto___type_7 : term -> Prop :=
    trans___type_7_i_1 : auto___type_7 i
  | trans___type_7_bob_1 : auto___type_7 bob
  | trans___type_7_server_1 : auto___type_7 server
  | trans___type_7_alice_1 : auto___type_7 alice
with auto___def_8 : term -> Prop :=
    trans___def_8_nai_1 : forall X1:term, auto_agent X1 -> auto___def_8 (nai X1)
with auto___def_97 : term -> Prop :=
    trans___def_97_cons_1 : forall X1 X2:term, auto___def_98 X1 -> auto___def_89 X2 -> auto___def_97 (cons X1 X2)
with auto_peer_keys_old : term -> term -> term -> Prop :=
    trans_peer_keys_old_1 : forall X1 X2 X3:term, auto___type_9 X1 -> auto___def_63 X2 -> auto___def_64 X3 -> auto_peer_keys_old X1 X2 X3
with auto___def_25 : term -> Prop :=
    trans___def_25_h_1 : forall X1:term, auto___def_26 X1 -> auto___def_25 (h X1)
with auto___def_112 : term -> Prop :=
    trans___def_112_cons_1 : forall X1 X2:term, auto___type_16 X1 -> auto___def_113 X2 -> auto___def_112 (cons X1 X2)
with auto___def_103 : term -> Prop :=
    trans___def_103_key_1 : forall X1 X2:term, auto___def_104 X1 -> auto___def_105 X2 -> auto___def_103 (key X1 X2)
with auto___def_23 : term -> Prop :=
    trans___def_23_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___def_23 (f1 X1 X2 X3)
with auto___type_5 : term -> Prop :=
    trans___type_5_i_1 : auto___type_5 i
  | trans___type_5_bob_1 : auto___type_5 bob
  | trans___type_5_server_1 : auto___type_5 server
  | trans___type_5_alice_1 : auto___type_5 alice
with auto___def_22 : term -> Prop :=
    trans___def_22_nil_1 : auto___def_22 nil
with auto___def_93 : term -> Prop :=
    trans___def_93_cons_1 : forall X1 X2:term, auto___def_79 X1 -> auto___def_99 X2 -> auto___def_93 (cons X1 X2)
with auto___def_24 : term -> Prop :=
    trans___def_24_nil_1 : auto___def_24 nil
with auto___def_10 : term -> Prop :=
    trans___def_10_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___def_10 (nonces_old X1 X2 X3)
with auto___def_102 : term -> Prop :=
    trans___def_102_cons_1 : forall X1 X2:term, auto___def_108 X1 -> auto___def_107 X2 -> auto___def_102 (cons X1 X2)
with auto___def_116 : term -> Prop :=
    trans___def_116_f3_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___def_116 (f3 X1 X2)
with auto___def_41 : term -> Prop :=
    trans___def_41_cons_1 : forall X1 X2:term, auto___type_5 X1 -> auto___def_42 X2 -> auto___def_41 (cons X1 X2)
with auto___def_28 : term -> Prop :=
    trans___def_28_cons_1 : forall X1 X2:term, auto___def_10 X1 -> auto___def_34 X2 -> auto___def_28 (cons X1 X2)
with auto_server_keys_old : term -> term -> term -> Prop :=
    trans_server_keys_old_1 : forall X1 X2 X3:term, auto___type_7 X1 -> auto___def_54 X2 -> auto___def_55 X3 -> auto_server_keys_old X1 X2 X3
with auto___def_42 : term -> Prop :=
    trans___def_42_nil_1 : auto___def_42 nil
with auto_knows_current : term -> Prop :=
    trans_knows_current_s_1 : forall X1:term, auto_knows_current X1 -> auto_knows_current (s X1)
  | trans_knows_current_nil_1 : auto_knows_current nil
  | trans_knows_current_f3_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto_knows_current (f3 X1 X2)
  | trans_knows_current_h_1 : forall X1:term, auto___def_109 X1 -> auto_knows_current (h X1)
  | trans_knows_current_h_2 : forall X1:term, auto___def_91 X1 -> auto_knows_current (h X1)
  | trans_knows_current_h_3 : forall X1:term, auto_knows_current X1 -> auto_knows_current (h X1)
  | trans_knows_current_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto_knows_current (nonces_current X1 X2 X3)
  | trans_knows_current_respond_id_1 : auto_knows_current respond_id
  | trans_knows_current_f2_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto_knows_current (f2 X1 X2)
  | trans_knows_current_success_1 : auto_knows_current success
  | trans_knows_current_request_id_1 : auto_knows_current request_id
  | trans_knows_current_crypt_1 : forall X1 X2:term, auto___def_85 X1 -> auto___def_86 X2 -> auto_knows_current (crypt X1 X2)
  | trans_knows_current_crypt_2 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto_knows_current (crypt X1 X2)
  | trans_knows_current_crypt_3 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto_knows_current (crypt X1 X2)
  | trans_knows_current_nai_1 : forall X1:term, auto_agent X1 -> auto_knows_current (nai X1)
  | trans_knows_current_f4_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto_knows_current (f4 X1 X2)
  | trans_knows_current_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto_knows_current (nonces_old X1 X2 X3)
  | trans_knows_current_cons_1 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto_knows_current (cons X1 X2)
  | trans_knows_current_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto_knows_current (f1 X1 X2 X3)
  | trans_knows_current_f1_2 : forall X1 X2 X3:term, auto___def_87 X1 -> auto___def_85 X2 -> auto___def_79 X3 -> auto_knows_current (f1 X1 X2 X3)
with auto___def_95 : term -> Prop :=
    trans___def_95_cons_1 : forall X1 X2:term, auto___def_96 X1 -> auto___def_97 X2 -> auto___def_95 (cons X1 X2)
with auto___def_107 : term -> Prop :=
    trans___def_107_nil_1 : auto___def_107 nil
with auto___def_18 : term -> Prop :=
    trans___def_18_key_1 : forall X1 X2:term, auto___def_19 X1 -> auto___def_20 X2 -> auto___def_18 (key X1 X2)
with auto___type_16 : term -> Prop :=
    trans___type_16_s_1 : forall X1:term, auto_knows_current X1 -> auto___type_16 (s X1)
  | trans___type_16_nil_1 : auto___type_16 nil
  | trans___type_16_f3_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___type_16 (f3 X1 X2)
  | trans___type_16_h_1 : forall X1:term, auto___def_109 X1 -> auto___type_16 (h X1)
  | trans___type_16_h_2 : forall X1:term, auto___def_91 X1 -> auto___type_16 (h X1)
  | trans___type_16_h_3 : forall X1:term, auto_knows_current X1 -> auto___type_16 (h X1)
  | trans___type_16_nonces_current_1 : forall X1 X2 X3:term, auto___def_78 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_16 (nonces_current X1 X2 X3)
  | trans___type_16_respond_id_1 : auto___type_16 respond_id
  | trans___type_16_f2_1 : forall X1 X2:term, auto___def_103 X1 -> auto___type_13 X2 -> auto___type_16 (f2 X1 X2)
  | trans___type_16_success_1 : auto___type_16 success
  | trans___type_16_request_id_1 : auto___type_16 request_id
  | trans___type_16_crypt_1 : forall X1 X2:term, auto___def_85 X1 -> auto___def_86 X2 -> auto___type_16 (crypt X1 X2)
  | trans___type_16_crypt_2 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___type_16 (crypt X1 X2)
  | trans___type_16_crypt_3 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto___type_16 (crypt X1 X2)
  | trans___type_16_nai_1 : forall X1:term, auto_agent X1 -> auto___type_16 (nai X1)
  | trans___type_16_f4_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___type_16 (f4 X1 X2)
  | trans___type_16_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto___type_16 (nonces_old X1 X2 X3)
  | trans___type_16_cons_1 : forall X1 X2:term, auto_knows_current X1 -> auto_knows_current X2 -> auto___type_16 (cons X1 X2)
  | trans___type_16_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto___type_16 (f1 X1 X2 X3)
  | trans___type_16_f1_2 : forall X1 X2 X3:term, auto___def_87 X1 -> auto___def_85 X2 -> auto___def_79 X3 -> auto___type_16 (f1 X1 X2 X3)
with auto___def_39 : term -> Prop :=
    trans___def_39_sym_1 : auto___def_39 sym
with auto___def_55 : term -> Prop :=
    trans___def_55_f3_1 : forall X1 X2:term, auto___def_56 X1 -> auto___def_57 X2 -> auto___def_55 (f3 X1 X2)
with auto_knows_old : term -> Prop :=
    trans_knows_old_s_1 : forall X1:term, auto_knows_old X1 -> auto_knows_old (s X1)
  | trans_knows_old_nil_1 : auto_knows_old nil
  | trans_knows_old_h_1 : forall X1:term, auto___def_44 X1 -> auto_knows_old (h X1)
  | trans_knows_old_h_2 : forall X1:term, auto___def_26 X1 -> auto_knows_old (h X1)
  | trans_knows_old_h_3 : forall X1:term, auto_knows_old X1 -> auto_knows_old (h X1)
  | trans_knows_old_respond_id_1 : auto_knows_old respond_id
  | trans_knows_old_f2_1 : forall X1 X2:term, auto___def_38 X1 -> auto___type_3 X2 -> auto_knows_old (f2 X1 X2)
  | trans_knows_old_success_1 : auto_knows_old success
  | trans_knows_old_request_id_1 : auto_knows_old request_id
  | trans_knows_old_crypt_1 : forall X1 X2:term, auto___def_16 X1 -> auto___def_17 X2 -> auto_knows_old (crypt X1 X2)
  | trans_knows_old_crypt_2 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto_knows_old (crypt X1 X2)
  | trans_knows_old_nai_1 : forall X1:term, auto_agent X1 -> auto_knows_old (nai X1)
  | trans_knows_old_nonces_old_1 : forall X1 X2 X3:term, auto___def_9 X1 -> auto_agent X2 -> auto_agent X3 -> auto_knows_old (nonces_old X1 X2 X3)
  | trans_knows_old_cons_1 : forall X1 X2:term, auto_knows_old X1 -> auto_knows_old X2 -> auto_knows_old (cons X1 X2)
  | trans_knows_old_f1_1 : forall X1 X2 X3:term, auto___def_18 X1 -> auto___def_16 X2 -> auto___def_10 X3 -> auto_knows_old (f1 X1 X2 X3)
with auto___query__intruder_knows_server_IK : Prop :=
with auto___query__intruder_knows_server_CK : Prop :=
.

(* [defp] Proofs that all definitions hold. *)


(* [appp] Proofs that all approximation clauses hold. *)


Inductive model_1 : Set := und_1:model_1 | val_1_1:model_1 | val_1_2:model_1 | val_1_3:model_1 | val_1_4:model_1 | val_1_5:model_1 | val_1_6:model_1 | val_1_7:model_1 | val_1_8:model_1 | val_1_9:model_1.

Definition seval_1_model_s (v1 : model_1) : model_1 :=
  match v1 with
      val_1_5 => val_1_5
    | _ => und_1
    end.

Remark seval_1_rewrite_s:forall X1 X2:model_1, X1=X2 -> (seval_1_model_s X1)=(seval_1_model_s X2).
Proof.
  intros X1 X2 H1. rewrite H1. reflexivity.
Qed.
Definition seval_1_model_key (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_1,val_1_2 => val_1_3
    | _,_ => und_1
    end.

Remark seval_1_rewrite_key:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_key X1 X2)=(seval_1_model_key X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_nil : model_1 := val_1_5.

Remark seval_1_rewrite_nil:seval_1_model_nil=seval_1_model_nil.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_i : model_1 := val_1_6.

Remark seval_1_rewrite_i:seval_1_model_i=seval_1_model_i.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_sym : model_1 := val_1_1.

Remark seval_1_rewrite_sym:seval_1_model_sym=seval_1_model_sym.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_f5 (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_3,val_1_5 => val_1_8
    | _,_ => und_1
    end.

Remark seval_1_rewrite_f5:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_f5 X1 X2)=(seval_1_model_f5 X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_session_old (v1 v2 v3 : model_1) : model_1 :=
  match v1,v2,v3 with
      val_1_5,val_1_6,val_1_6 => val_1_4
    | _,_,_ => und_1
    end.

Remark seval_1_rewrite_session_old:forall X1 X2 X3 X4 X5 X6:model_1, X1=X4 -> X2=X5 -> X3=X6 -> (seval_1_model_session_old X1 X2 X3)=(seval_1_model_session_old X4 X5 X6).
Proof.
  intros X1 X2 X3 X4 X5 X6 H1 H2 H3. rewrite H1. rewrite H2. rewrite H3. reflexivity.
Qed.
Definition seval_1_model_f3 (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_3,val_1_5 => val_1_5
    | _,_ => und_1
    end.

Remark seval_1_rewrite_f3:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_f3 X1 X2)=(seval_1_model_f3 X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_h (v1 : model_1) : model_1 :=
  match v1 with
      val_1_5 => val_1_5
    | _ => und_1
    end.

Remark seval_1_rewrite_h:forall X1 X2:model_1, X1=X2 -> (seval_1_model_h X1)=(seval_1_model_h X2).
Proof.
  intros X1 X2 H1. rewrite H1. reflexivity.
Qed.
Definition seval_1_model_nonces_current (v1 v2 v3 : model_1) : model_1 :=
  match v1,v2,v3 with
      val_1_5,val_1_6,val_1_6 => val_1_5
    | _,_,_ => und_1
    end.

Remark seval_1_rewrite_nonces_current:forall X1 X2 X3 X4 X5 X6:model_1, X1=X4 -> X2=X5 -> X3=X6 -> (seval_1_model_nonces_current X1 X2 X3)=(seval_1_model_nonces_current X4 X5 X6).
Proof.
  intros X1 X2 X3 X4 X5 X6 H1 H2 H3. rewrite H1. rewrite H2. rewrite H3. reflexivity.
Qed.
Definition seval_1_model_session_current (v1 v2 v3 : model_1) : model_1 :=
  match v1,v2,v3 with
      val_1_5,val_1_6,val_1_6 => val_1_7
    | _,_,_ => und_1
    end.

Remark seval_1_rewrite_session_current:forall X1 X2 X3 X4 X5 X6:model_1, X1=X4 -> X2=X5 -> X3=X6 -> (seval_1_model_session_current X1 X2 X3)=(seval_1_model_session_current X4 X5 X6).
Proof.
  intros X1 X2 X3 X4 X5 X6 H1 H2 H3. rewrite H1. rewrite H2. rewrite H3. reflexivity.
Qed.
Definition seval_1_model_respond_id : model_1 := val_1_5.

Remark seval_1_rewrite_respond_id:seval_1_model_respond_id=seval_1_model_respond_id.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_f2 (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_3,val_1_5 => val_1_5
    | _,_ => und_1
    end.

Remark seval_1_rewrite_f2:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_f2 X1 X2)=(seval_1_model_f2 X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_success : model_1 := val_1_5.

Remark seval_1_rewrite_success:seval_1_model_success=seval_1_model_success.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_request_id : model_1 := val_1_5.

Remark seval_1_rewrite_request_id:seval_1_model_request_id=seval_1_model_request_id.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_crypt (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_7,val_1_8 => val_1_5
    | val_1_4,val_1_8 => val_1_5
    | val_1_5,val_1_5 => val_1_5
    | _,_ => und_1
    end.

Remark seval_1_rewrite_crypt:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_crypt X1 X2)=(seval_1_model_crypt X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_nai (v1 : model_1) : model_1 :=
  match v1 with
      val_1_6 => val_1_5
    | _ => und_1
    end.

Remark seval_1_rewrite_nai:forall X1 X2:model_1, X1=X2 -> (seval_1_model_nai X1)=(seval_1_model_nai X2).
Proof.
  intros X1 X2 H1. rewrite H1. reflexivity.
Qed.
Definition seval_1_model_f4 (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_3,val_1_5 => val_1_5
    | _,_ => und_1
    end.

Remark seval_1_rewrite_f4:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_f4 X1 X2)=(seval_1_model_f4 X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_bob : model_1 := val_1_6.

Remark seval_1_rewrite_bob:seval_1_model_bob=seval_1_model_bob.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_server : model_1 := val_1_6.

Remark seval_1_rewrite_server:seval_1_model_server=seval_1_model_server.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_nonces_old (v1 v2 v3 : model_1) : model_1 :=
  match v1,v2,v3 with
      val_1_5,val_1_6,val_1_6 => val_1_5
    | _,_,_ => und_1
    end.

Remark seval_1_rewrite_nonces_old:forall X1 X2 X3 X4 X5 X6:model_1, X1=X4 -> X2=X5 -> X3=X6 -> (seval_1_model_nonces_old X1 X2 X3)=(seval_1_model_nonces_old X4 X5 X6).
Proof.
  intros X1 X2 X3 X4 X5 X6 H1 H2 H3. rewrite H1. rewrite H2. rewrite H3. reflexivity.
Qed.
Definition seval_1_model_cons (v1 v2 : model_1) : model_1 :=
  match v1,v2 with
      val_1_5,val_1_5 => val_1_5
    | val_1_6,val_1_9 => val_1_2
    | val_1_6,val_1_5 => val_1_9
    | _,_ => und_1
    end.

Remark seval_1_rewrite_cons:forall X1 X2 X3 X4:model_1, X1=X3 -> X2=X4 -> (seval_1_model_cons X1 X2)=(seval_1_model_cons X3 X4).
Proof.
  intros X1 X2 X3 X4 H1 H2. rewrite H1. rewrite H2. reflexivity.
Qed.
Definition seval_1_model_alice : model_1 := val_1_6.

Remark seval_1_rewrite_alice:seval_1_model_alice=seval_1_model_alice.
Proof.
  reflexivity.
Qed.

Definition seval_1_model_f1 (v1 v2 v3 : model_1) : model_1 :=
  match v1,v2,v3 with
      val_1_3,val_1_7,val_1_5 => val_1_5
    | val_1_3,val_1_4,val_1_5 => val_1_5
    | _,_,_ => und_1
    end.

Remark seval_1_rewrite_f1:forall X1 X2 X3 X4 X5 X6:model_1, X1=X4 -> X2=X5 -> X3=X6 -> (seval_1_model_f1 X1 X2 X3)=(seval_1_model_f1 X4 X5 X6).
Proof.
  intros X1 X2 X3 X4 X5 X6 H1 H2 H3. rewrite H1. rewrite H2. rewrite H3. reflexivity.
Qed.
Fixpoint seval_1 (t : term) {struct t} : model_1 :=
  match t  with
    | (s X1) => (seval_1_model_s (seval_1 X1))
  | (key X1 X2) => (seval_1_model_key (seval_1 X1) (seval_1 X2))
  | nil => (seval_1_model_nil)
  | i => (seval_1_model_i)
  | sym => (seval_1_model_sym)
  | (f5 X1 X2) => (seval_1_model_f5 (seval_1 X1) (seval_1 X2))
  | (session_old X1 X2 X3) => (seval_1_model_session_old (seval_1 X1) (seval_1 X2) (seval_1 X3))
  | (f3 X1 X2) => (seval_1_model_f3 (seval_1 X1) (seval_1 X2))
  | (h X1) => (seval_1_model_h (seval_1 X1))
  | (nonces_current X1 X2 X3) => (seval_1_model_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3))
  | (session_current X1 X2 X3) => (seval_1_model_session_current (seval_1 X1) (seval_1 X2) (seval_1 X3))
  | respond_id => (seval_1_model_respond_id)
  | (f2 X1 X2) => (seval_1_model_f2 (seval_1 X1) (seval_1 X2))
  | success => (seval_1_model_success)
  | request_id => (seval_1_model_request_id)
  | (crypt X1 X2) => (seval_1_model_crypt (seval_1 X1) (seval_1 X2))
  | (nai X1) => (seval_1_model_nai (seval_1 X1))
  | (f4 X1 X2) => (seval_1_model_f4 (seval_1 X1) (seval_1 X2))
  | bob => (seval_1_model_bob)
  | server => (seval_1_model_server)
  | (nonces_old X1 X2 X3) => (seval_1_model_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3))
  | (cons X1 X2) => (seval_1_model_cons (seval_1 X1) (seval_1 X2))
  | alice => (seval_1_model_alice)
  | (f1 X1 X2 X3) => (seval_1_model_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3))
  | _  => und_1
  end.

Definition seval_1_model_auto___type_11 (X:term) (pi:(auto___type_11 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_11 X) return (seval_1 X)=val_1_6 with
    (trans___type_11_i_1) => (seval_1_rewrite_i)
  | (trans___type_11_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_11_server_1) => (seval_1_rewrite_server)
  | (trans___type_11_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_123 (X:term) (pi:(auto___def_123 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_123 X) return (seval_1 X)=val_1_1 with
    (trans___def_123_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_107 (X:term) (pi:(auto___def_107 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_107 X) return (seval_1 X)=val_1_5 with
    (trans___def_107_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___type_15 (X:term) (pi:(auto___type_15 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_15 X) return (seval_1 X)=val_1_6 with
    (trans___type_15_i_1) => (seval_1_rewrite_i)
  | (trans___type_15_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_15_server_1) => (seval_1_rewrite_server)
  | (trans___type_15_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_106 (X:term) (pi:(auto___def_106 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_106 X) return (seval_1 X)=val_1_9 with
    (trans___def_106_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto___type_15 X1 H1) (seval_1_model_auto___def_107 X2 H2))
  end
.
Definition seval_1_model_auto___type_14 (X:term) (pi:(auto___type_14 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_14 X) return (seval_1 X)=val_1_6 with
    (trans___type_14_i_1) => (seval_1_rewrite_i)
  | (trans___type_14_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_14_server_1) => (seval_1_rewrite_server)
  | (trans___type_14_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_105 (X:term) (pi:(auto___def_105 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_105 X) return (seval_1 X)=val_1_2 with
    (trans___def_105_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_14 X1 H1) (seval_1_model_auto___def_106 X2 H2))
  end
.
Definition seval_1_model_auto_agent (X:term) (pi:(auto_agent X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto_agent X) return (seval_1 X)=val_1_6 with
    (trans_agent_i_1) => (seval_1_rewrite_i)
  | (trans_agent_bob_1) => (seval_1_rewrite_bob)
  | (trans_agent_server_1) => (seval_1_rewrite_server)
  | (trans_agent_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___type_4 (X:term) (pi:(auto___type_4 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_4 X) return (seval_1 X)=val_1_6 with
    (trans___type_4_i_1) => (seval_1_rewrite_i)
  | (trans___type_4_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_4_server_1) => (seval_1_rewrite_server)
  | (trans___type_4_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_42 (X:term) (pi:(auto___def_42 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_42 X) return (seval_1 X)=val_1_5 with
    (trans___def_42_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___def_24 (X:term) (pi:(auto___def_24 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_24 X) return (seval_1 X)=val_1_5 with
    (trans___def_24_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___def_19 (X:term) (pi:(auto___def_19 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_19 X) return (seval_1 X)=val_1_1 with
    (trans___def_19_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_22 (X:term) (pi:(auto___def_22 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_22 X) return (seval_1 X)=val_1_5 with
    (trans___def_22_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___def_21 (X:term) (pi:(auto___def_21 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_21 X) return (seval_1 X)=val_1_9 with
    (trans___def_21_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto_agent X1 H1) (seval_1_model_auto___def_22 X2 H2))
  end
.
Definition seval_1_model_auto___type_1 (X:term) (pi:(auto___type_1 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_1 X) return (seval_1 X)=val_1_6 with
    (trans___type_1_i_1) => (seval_1_rewrite_i)
  | (trans___type_1_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_1_server_1) => (seval_1_rewrite_server)
  | (trans___type_1_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_20 (X:term) (pi:(auto___def_20 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_20 X) return (seval_1 X)=val_1_2 with
    (trans___def_20_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_1 X1 H1) (seval_1_model_auto___def_21 X2 H2))
  end
.
Definition seval_1_model_auto___def_18 (X:term) (pi:(auto___def_18 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_18 X) return (seval_1 X)=val_1_3 with
    (trans___def_18_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_19 X1 H1) (seval_1_model_auto___def_20 X2 H2))
  end
.
Definition seval_1_model_auto___type_5 (X:term) (pi:(auto___type_5 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_5 X) return (seval_1 X)=val_1_6 with
    (trans___type_5_i_1) => (seval_1_rewrite_i)
  | (trans___type_5_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_5_server_1) => (seval_1_rewrite_server)
  | (trans___type_5_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_41 (X:term) (pi:(auto___def_41 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_41 X) return (seval_1 X)=val_1_9 with
    (trans___def_41_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto___type_5 X1 H1) (seval_1_model_auto___def_42 X2 H2))
  end
.
Definition seval_1_model_auto___def_40 (X:term) (pi:(auto___def_40 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_40 X) return (seval_1 X)=val_1_2 with
    (trans___def_40_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_4 X1 H1) (seval_1_model_auto___def_41 X2 H2))
  end
.
Definition seval_1_model_auto___def_39 (X:term) (pi:(auto___def_39 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_39 X) return (seval_1 X)=val_1_1 with
    (trans___def_39_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_38 (X:term) (pi:(auto___def_38 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_38 X) return (seval_1 X)=val_1_3 with
    (trans___def_38_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_39 X1 H1) (seval_1_model_auto___def_40 X2 H2))
  end
.
Fixpoint seval_1_model_auto___def_10 (X:term) (pi:(auto___def_10 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_10 X) return (seval_1 X)=val_1_5 with
    (trans___def_10_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___def_12 (X:term) (pi:(auto___def_12 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_12 X) return (seval_1 X)=val_1_5 with
    (trans___def_12_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_14 X1 H1) (seval_1_model_auto___def_15 X2 H2))
  end

with seval_1_model_auto___def_14 (X:term) (pi:(auto___def_14 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_14 X) return (seval_1 X)=val_1_5 with
    (trans___def_14_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  end

with seval_1_model_auto___def_15 (X:term) (pi:(auto___def_15 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_15 X) return (seval_1 X)=val_1_5 with
    (trans___def_15_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_23 X1 H1) (seval_1_model_auto___def_24 X2 H2))
  end

with seval_1_model_auto___def_16 (X:term) (pi:(auto___def_16 X)) {struct pi}:((seval_1 X)=val_1_4) :=
  match pi as pi in (auto___def_16 X) return (seval_1 X)=val_1_4 with
    (trans___def_16_session_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_session_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___def_17 (X:term) (pi:(auto___def_17 X)) {struct pi}:((seval_1 X)=val_1_8) :=
  match pi as pi in (auto___def_17 X) return (seval_1 X)=val_1_8 with
    (trans___def_17_f5_1 X1 X2 H1 H2) => (seval_1_rewrite_f5 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_10 X2 H2))
  end

with seval_1_model_auto___def_23 (X:term) (pi:(auto___def_23 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_23 X) return (seval_1 X)=val_1_5 with
    (trans___def_23_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  end

with seval_1_model_auto___def_26 (X:term) (pi:(auto___def_26 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_26 X) return (seval_1 X)=val_1_5 with
    (trans___def_26_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_27 X1 H1) (seval_1_model_auto___def_28 X2 H2))
  end

with seval_1_model_auto___def_27 (X:term) (pi:(auto___def_27 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_27 X) return (seval_1 X)=val_1_5 with
    (trans___def_27_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_29 X1 H1))
  end

with seval_1_model_auto___def_28 (X:term) (pi:(auto___def_28 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_28 X) return (seval_1 X)=val_1_5 with
    (trans___def_28_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_10 X1 H1) (seval_1_model_auto___def_34 X2 H2))
  end

with seval_1_model_auto___def_29 (X:term) (pi:(auto___def_29 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_29 X) return (seval_1 X)=val_1_5 with
    (trans___def_29_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___type_2 X1 H1) (seval_1_model_auto___def_30 X2 H2))
  end

with seval_1_model_auto___def_30 (X:term) (pi:(auto___def_30 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_30 X) return (seval_1 X)=val_1_5 with
    (trans___def_30_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_31 X1 H1) (seval_1_model_auto___def_32 X2 H2))
  end

with seval_1_model_auto___def_31 (X:term) (pi:(auto___def_31 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_31 X) return (seval_1 X)=val_1_5 with
    (trans___def_31_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_10 X2 H2))
  end

with seval_1_model_auto___def_32 (X:term) (pi:(auto___def_32 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_32 X) return (seval_1 X)=val_1_5 with
    (trans___def_32_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_33 X1 H1) (seval_1_model_auto___def_24 X2 H2))
  end

with seval_1_model_auto___def_33 (X:term) (pi:(auto___def_33 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_33 X) return (seval_1 X)=val_1_5 with
    (trans___def_33_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_10 X2 H2))
  end

with seval_1_model_auto___def_34 (X:term) (pi:(auto___def_34 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_34 X) return (seval_1 X)=val_1_5 with
    (trans___def_34_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_12 X1 H1) (seval_1_model_auto___def_24 X2 H2))
  end

with seval_1_model_auto___def_36 (X:term) (pi:(auto___def_36 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_36 X) return (seval_1 X)=val_1_5 with
    (trans___def_36_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  end

with seval_1_model_auto___def_44 (X:term) (pi:(auto___def_44 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_44 X) return (seval_1 X)=val_1_5 with
    (trans___def_44_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_45 X1 H1) (seval_1_model_auto___def_46 X2 H2))
  end

with seval_1_model_auto___def_45 (X:term) (pi:(auto___def_45 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_45 X) return (seval_1 X)=val_1_5 with
    (trans___def_45_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_47 X1 H1))
  end

with seval_1_model_auto___def_46 (X:term) (pi:(auto___def_46 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_46 X) return (seval_1 X)=val_1_5 with
    (trans___def_46_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_36 X1 H1) (seval_1_model_auto___def_42 X2 H2))
  end

with seval_1_model_auto___def_47 (X:term) (pi:(auto___def_47 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_47 X) return (seval_1 X)=val_1_5 with
    (trans___def_47_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___type_6 X1 H1) (seval_1_model_auto___def_48 X2 H2))
  end

with seval_1_model_auto___def_48 (X:term) (pi:(auto___def_48 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_48 X) return (seval_1 X)=val_1_5 with
    (trans___def_48_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_49 X1 H1) (seval_1_model_auto___def_50 X2 H2))
  end

with seval_1_model_auto___def_49 (X:term) (pi:(auto___def_49 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_49 X) return (seval_1 X)=val_1_5 with
    (trans___def_49_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  end

with seval_1_model_auto___def_50 (X:term) (pi:(auto___def_50 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_50 X) return (seval_1 X)=val_1_5 with
    (trans___def_50_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_51 X1 H1) (seval_1_model_auto___def_42 X2 H2))
  end

with seval_1_model_auto___def_51 (X:term) (pi:(auto___def_51 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_51 X) return (seval_1 X)=val_1_5 with
    (trans___def_51_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  end

with seval_1_model_auto___def_9 (X:term) (pi:(auto___def_9 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_9 X) return (seval_1 X)=val_1_5 with
    (trans___def_9_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___def_9_nil_1) => (seval_1_rewrite_nil)
  | (trans___def_9_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_44 X1 H1))
  | (trans___def_9_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_26 X1 H1))
  | (trans___def_9_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___def_9_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___def_9_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  | (trans___def_9_success_1) => (seval_1_rewrite_success)
  | (trans___def_9_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___def_9_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___def_9_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___def_9_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___def_9_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___def_9_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___def_9_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  end

with seval_1_model_auto___type_2 (X:term) (pi:(auto___type_2 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_2 X) return (seval_1 X)=val_1_5 with
    (trans___type_2_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___type_2_nil_1) => (seval_1_rewrite_nil)
  | (trans___type_2_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_44 X1 H1))
  | (trans___type_2_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_26 X1 H1))
  | (trans___type_2_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___type_2_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___type_2_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  | (trans___type_2_success_1) => (seval_1_rewrite_success)
  | (trans___type_2_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___type_2_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___type_2_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___type_2_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___type_2_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_2_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___type_2_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  end

with seval_1_model_auto___type_3 (X:term) (pi:(auto___type_3 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_3 X) return (seval_1 X)=val_1_5 with
    (trans___type_3_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___type_6 (X:term) (pi:(auto___type_6 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_6 X) return (seval_1 X)=val_1_5 with
    (trans___type_6_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___type_6_nil_1) => (seval_1_rewrite_nil)
  | (trans___type_6_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_44 X1 H1))
  | (trans___type_6_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_26 X1 H1))
  | (trans___type_6_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans___type_6_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___type_6_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  | (trans___type_6_success_1) => (seval_1_rewrite_success)
  | (trans___type_6_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___type_6_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___type_6_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___type_6_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___type_6_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_6_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans___type_6_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  end

with seval_1_model_auto_knows_old (X:term) (pi:(auto_knows_old X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto_knows_old X) return (seval_1 X)=val_1_5 with
    (trans_knows_old_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans_knows_old_nil_1) => (seval_1_rewrite_nil)
  | (trans_knows_old_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_44 X1 H1))
  | (trans_knows_old_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_26 X1 H1))
  | (trans_knows_old_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_old X1 H1))
  | (trans_knows_old_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans_knows_old_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_38 X1 H1) (seval_1_model_auto___type_3 X2 H2))
  | (trans_knows_old_success_1) => (seval_1_rewrite_success)
  | (trans_knows_old_request_id_1) => (seval_1_rewrite_request_id)
  | (trans_knows_old_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans_knows_old_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans_knows_old_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans_knows_old_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans_knows_old_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_old X1 H1) (seval_1_model_auto_knows_old X2 H2))
  | (trans_knows_old_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  end
.
Definition seval_1_model_auto___def_57 (X:term) (pi:(auto___def_57 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_57 X) return (seval_1 X)=val_1_5 with
    (trans___def_57_nonces_old_1 X1 X2 X3 H1 _ H2 _ H3 _) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___type_6 X1 H1) (seval_1_model_auto___type_4 X2 H2) (seval_1_model_auto_agent X3 H3))
  end
.
Definition seval_1_model_auto___def_104 (X:term) (pi:(auto___def_104 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_104 X) return (seval_1 X)=val_1_1 with
    (trans___def_104_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_103 (X:term) (pi:(auto___def_103 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_103 X) return (seval_1 X)=val_1_3 with
    (trans___def_103_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_104 X1 H1) (seval_1_model_auto___def_105 X2 H2))
  end
.
Definition seval_1_model_auto___def_89 (X:term) (pi:(auto___def_89 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_89 X) return (seval_1 X)=val_1_5 with
    (trans___def_89_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___type_7 (X:term) (pi:(auto___type_7 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_7 X) return (seval_1 X)=val_1_6 with
    (trans___type_7_i_1) => (seval_1_rewrite_i)
  | (trans___type_7_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_7_server_1) => (seval_1_rewrite_server)
  | (trans___type_7_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_61 (X:term) (pi:(auto___def_61 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_61 X) return (seval_1 X)=val_1_5 with
    (trans___def_61_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___type_8 (X:term) (pi:(auto___type_8 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_8 X) return (seval_1 X)=val_1_6 with
    (trans___type_8_i_1) => (seval_1_rewrite_i)
  | (trans___type_8_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_8_server_1) => (seval_1_rewrite_server)
  | (trans___type_8_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_60 (X:term) (pi:(auto___def_60 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_60 X) return (seval_1 X)=val_1_9 with
    (trans___def_60_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto___type_8 X1 H1) (seval_1_model_auto___def_61 X2 H2))
  end
.
Definition seval_1_model_auto___def_59 (X:term) (pi:(auto___def_59 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_59 X) return (seval_1 X)=val_1_2 with
    (trans___def_59_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_7 X1 H1) (seval_1_model_auto___def_60 X2 H2))
  end
.
Definition seval_1_model_auto___def_58 (X:term) (pi:(auto___def_58 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_58 X) return (seval_1 X)=val_1_1 with
    (trans___def_58_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_56 (X:term) (pi:(auto___def_56 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_56 X) return (seval_1 X)=val_1_3 with
    (trans___def_56_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_58 X1 H1) (seval_1_model_auto___def_59 X2 H2))
  end
.
Definition seval_1_model_auto___def_87 (X:term) (pi:(auto___def_87 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_87 X) return (seval_1 X)=val_1_3 with
    (trans___def_87_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_19 X1 H1) (seval_1_model_auto___def_20 X2 H2))
  end
.
Fixpoint seval_1_model_auto___def_101 (X:term) (pi:(auto___def_101 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_101 X) return (seval_1 X)=val_1_5 with
    (trans___def_101_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  end

with seval_1_model_auto___def_109 (X:term) (pi:(auto___def_109 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_109 X) return (seval_1 X)=val_1_5 with
    (trans___def_109_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_110 X1 H1) (seval_1_model_auto___def_111 X2 H2))
  end

with seval_1_model_auto___def_110 (X:term) (pi:(auto___def_110 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_110 X) return (seval_1 X)=val_1_5 with
    (trans___def_110_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_112 X1 H1))
  end

with seval_1_model_auto___def_111 (X:term) (pi:(auto___def_111 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_111 X) return (seval_1 X)=val_1_5 with
    (trans___def_111_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_101 X1 H1) (seval_1_model_auto___def_107 X2 H2))
  end

with seval_1_model_auto___def_112 (X:term) (pi:(auto___def_112 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_112 X) return (seval_1 X)=val_1_5 with
    (trans___def_112_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___type_16 X1 H1) (seval_1_model_auto___def_113 X2 H2))
  end

with seval_1_model_auto___def_113 (X:term) (pi:(auto___def_113 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_113 X) return (seval_1 X)=val_1_5 with
    (trans___def_113_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_114 X1 H1) (seval_1_model_auto___def_115 X2 H2))
  end

with seval_1_model_auto___def_114 (X:term) (pi:(auto___def_114 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_114 X) return (seval_1 X)=val_1_5 with
    (trans___def_114_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  end

with seval_1_model_auto___def_115 (X:term) (pi:(auto___def_115 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_115 X) return (seval_1 X)=val_1_5 with
    (trans___def_115_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_116 X1 H1) (seval_1_model_auto___def_107 X2 H2))
  end

with seval_1_model_auto___def_116 (X:term) (pi:(auto___def_116 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_116 X) return (seval_1 X)=val_1_5 with
    (trans___def_116_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  end

with seval_1_model_auto___def_78 (X:term) (pi:(auto___def_78 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_78 X) return (seval_1 X)=val_1_5 with
    (trans___def_78_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___def_78_nil_1) => (seval_1_rewrite_nil)
  | (trans___def_78_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___def_78_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_109 X1 H1))
  | (trans___def_78_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_91 X1 H1))
  | (trans___def_78_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___def_78_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___def_78_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___def_78_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  | (trans___def_78_success_1) => (seval_1_rewrite_success)
  | (trans___def_78_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___def_78_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_7 val_1_8 (seval_1_model_auto___def_85 X1 H1) (seval_1_model_auto___def_86 X2 H2))
  | (trans___def_78_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___def_78_crypt_3 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___def_78_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___def_78_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___def_78_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___def_78_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___def_78_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  | (trans___def_78_f1_2 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_7 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_85 X2 H2) (seval_1_model_auto___def_79 X3 H3))
  end

with seval_1_model_auto___def_79 (X:term) (pi:(auto___def_79 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_79 X) return (seval_1 X)=val_1_5 with
    (trans___def_79_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___def_81 (X:term) (pi:(auto___def_81 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_81 X) return (seval_1 X)=val_1_5 with
    (trans___def_81_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_83 X1 H1) (seval_1_model_auto___def_84 X2 H2))
  end

with seval_1_model_auto___def_83 (X:term) (pi:(auto___def_83 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_83 X) return (seval_1 X)=val_1_5 with
    (trans___def_83_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_7 val_1_8 (seval_1_model_auto___def_85 X1 H1) (seval_1_model_auto___def_86 X2 H2))
  end

with seval_1_model_auto___def_84 (X:term) (pi:(auto___def_84 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_84 X) return (seval_1 X)=val_1_5 with
    (trans___def_84_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_88 X1 H1) (seval_1_model_auto___def_89 X2 H2))
  end

with seval_1_model_auto___def_85 (X:term) (pi:(auto___def_85 X)) {struct pi}:((seval_1 X)=val_1_7) :=
  match pi as pi in (auto___def_85 X) return (seval_1 X)=val_1_7 with
    (trans___def_85_session_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_session_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___def_86 (X:term) (pi:(auto___def_86 X)) {struct pi}:((seval_1 X)=val_1_8) :=
  match pi as pi in (auto___def_86 X) return (seval_1 X)=val_1_8 with
    (trans___def_86_f5_1 X1 X2 H1 H2) => (seval_1_rewrite_f5 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_79 X2 H2))
  end

with seval_1_model_auto___def_88 (X:term) (pi:(auto___def_88 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_88 X) return (seval_1 X)=val_1_5 with
    (trans___def_88_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_7 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_85 X2 H2) (seval_1_model_auto___def_79 X3 H3))
  end

with seval_1_model_auto___def_91 (X:term) (pi:(auto___def_91 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_91 X) return (seval_1 X)=val_1_5 with
    (trans___def_91_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_92 X1 H1) (seval_1_model_auto___def_93 X2 H2))
  end

with seval_1_model_auto___def_92 (X:term) (pi:(auto___def_92 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_92 X) return (seval_1 X)=val_1_5 with
    (trans___def_92_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_94 X1 H1))
  end

with seval_1_model_auto___def_93 (X:term) (pi:(auto___def_93 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_93 X) return (seval_1 X)=val_1_5 with
    (trans___def_93_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_79 X1 H1) (seval_1_model_auto___def_99 X2 H2))
  end

with seval_1_model_auto___def_94 (X:term) (pi:(auto___def_94 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_94 X) return (seval_1 X)=val_1_5 with
    (trans___def_94_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___type_12 X1 H1) (seval_1_model_auto___def_95 X2 H2))
  end

with seval_1_model_auto___def_95 (X:term) (pi:(auto___def_95 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_95 X) return (seval_1 X)=val_1_5 with
    (trans___def_95_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_96 X1 H1) (seval_1_model_auto___def_97 X2 H2))
  end

with seval_1_model_auto___def_96 (X:term) (pi:(auto___def_96 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_96 X) return (seval_1 X)=val_1_5 with
    (trans___def_96_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_79 X2 H2))
  end

with seval_1_model_auto___def_97 (X:term) (pi:(auto___def_97 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_97 X) return (seval_1 X)=val_1_5 with
    (trans___def_97_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_98 X1 H1) (seval_1_model_auto___def_89 X2 H2))
  end

with seval_1_model_auto___def_98 (X:term) (pi:(auto___def_98 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_98 X) return (seval_1 X)=val_1_5 with
    (trans___def_98_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_79 X2 H2))
  end

with seval_1_model_auto___def_99 (X:term) (pi:(auto___def_99 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_99 X) return (seval_1 X)=val_1_5 with
    (trans___def_99_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_81 X1 H1) (seval_1_model_auto___def_89 X2 H2))
  end

with seval_1_model_auto___type_12 (X:term) (pi:(auto___type_12 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_12 X) return (seval_1 X)=val_1_5 with
    (trans___type_12_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___type_12_nil_1) => (seval_1_rewrite_nil)
  | (trans___type_12_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___type_12_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_109 X1 H1))
  | (trans___type_12_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_91 X1 H1))
  | (trans___type_12_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___type_12_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_12_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___type_12_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  | (trans___type_12_success_1) => (seval_1_rewrite_success)
  | (trans___type_12_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___type_12_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_7 val_1_8 (seval_1_model_auto___def_85 X1 H1) (seval_1_model_auto___def_86 X2 H2))
  | (trans___type_12_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___type_12_crypt_3 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___type_12_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___type_12_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___type_12_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_12_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___type_12_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  | (trans___type_12_f1_2 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_7 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_85 X2 H2) (seval_1_model_auto___def_79 X3 H3))
  end

with seval_1_model_auto___type_13 (X:term) (pi:(auto___type_13 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_13 X) return (seval_1 X)=val_1_5 with
    (trans___type_13_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_13_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end

with seval_1_model_auto___type_16 (X:term) (pi:(auto___type_16 X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_16 X) return (seval_1 X)=val_1_5 with
    (trans___type_16_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___type_16_nil_1) => (seval_1_rewrite_nil)
  | (trans___type_16_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___type_16_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_109 X1 H1))
  | (trans___type_16_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_91 X1 H1))
  | (trans___type_16_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans___type_16_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_16_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans___type_16_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  | (trans___type_16_success_1) => (seval_1_rewrite_success)
  | (trans___type_16_request_id_1) => (seval_1_rewrite_request_id)
  | (trans___type_16_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_7 val_1_8 (seval_1_model_auto___def_85 X1 H1) (seval_1_model_auto___def_86 X2 H2))
  | (trans___type_16_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___type_16_crypt_3 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans___type_16_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans___type_16_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans___type_16_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans___type_16_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans___type_16_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  | (trans___type_16_f1_2 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_7 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_85 X2 H2) (seval_1_model_auto___def_79 X3 H3))
  end

with seval_1_model_auto_knows_current (X:term) (pi:(auto_knows_current X)) {struct pi}:((seval_1 X)=val_1_5) :=
  match pi as pi in (auto_knows_current X) return (seval_1 X)=val_1_5 with
    (trans_knows_current_s_1 X1 H1) => (seval_1_rewrite_s (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans_knows_current_nil_1) => (seval_1_rewrite_nil)
  | (trans_knows_current_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans_knows_current_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_109 X1 H1))
  | (trans_knows_current_h_2 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_91 X1 H1))
  | (trans_knows_current_h_3 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto_knows_current X1 H1))
  | (trans_knows_current_nonces_current_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_78 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans_knows_current_respond_id_1) => (seval_1_rewrite_respond_id)
  | (trans_knows_current_f2_1 X1 X2 H1 H2) => (seval_1_rewrite_f2 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_103 X1 H1) (seval_1_model_auto___type_13 X2 H2))
  | (trans_knows_current_success_1) => (seval_1_rewrite_success)
  | (trans_knows_current_request_id_1) => (seval_1_rewrite_request_id)
  | (trans_knows_current_crypt_1 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_7 val_1_8 (seval_1_model_auto___def_85 X1 H1) (seval_1_model_auto___def_86 X2 H2))
  | (trans_knows_current_crypt_2 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans_knows_current_crypt_3 X1 X2 H1 H2) => (seval_1_rewrite_crypt (seval_1 X1) (seval_1 X2) val_1_4 val_1_8 (seval_1_model_auto___def_16 X1 H1) (seval_1_model_auto___def_17 X2 H2))
  | (trans_knows_current_nai_1 X1 H1) => (seval_1_rewrite_nai (seval_1 X1) val_1_6 (seval_1_model_auto_agent X1 H1))
  | (trans_knows_current_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  | (trans_knows_current_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  | (trans_knows_current_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto_knows_current X2 H2))
  | (trans_knows_current_f1_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_4 val_1_5 (seval_1_model_auto___def_18 X1 H1) (seval_1_model_auto___def_16 X2 H2) (seval_1_model_auto___def_10 X3 H3))
  | (trans_knows_current_f1_2 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_f1 (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_3 val_1_7 val_1_5 (seval_1_model_auto___def_87 X1 H1) (seval_1_model_auto___def_85 X2 H2) (seval_1_model_auto___def_79 X3 H3))
  end
.
Definition seval_1_model_auto___def_122 (X:term) (pi:(auto___def_122 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_122 X) return (seval_1 X)=val_1_5 with
    (trans___def_122_nonces_current_1 X1 X2 X3 H1 H2 _ H3 _) => (seval_1_rewrite_nonces_current (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto_knows_current X1 H1) (seval_1_model_auto___type_14 X2 H2) (seval_1_model_auto___type_15 X3 H3))
  end
.
Definition seval_1_model_auto___type_18 (X:term) (pi:(auto___type_18 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_18 X) return (seval_1 X)=val_1_6 with
    (trans___type_18_i_1) => (seval_1_rewrite_i)
  | (trans___type_18_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_18_server_1) => (seval_1_rewrite_server)
  | (trans___type_18_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_126 (X:term) (pi:(auto___def_126 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_126 X) return (seval_1 X)=val_1_5 with
    (trans___def_126_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___def_125 (X:term) (pi:(auto___def_125 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_125 X) return (seval_1 X)=val_1_9 with
    (trans___def_125_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto___type_18 X1 H1) (seval_1_model_auto___def_126 X2 H2))
  end
.
Definition seval_1_model_auto___type_17 (X:term) (pi:(auto___type_17 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_17 X) return (seval_1 X)=val_1_6 with
    (trans___type_17_i_1) => (seval_1_rewrite_i)
  | (trans___type_17_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_17_server_1) => (seval_1_rewrite_server)
  | (trans___type_17_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___def_124 (X:term) (pi:(auto___def_124 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_124 X) return (seval_1 X)=val_1_2 with
    (trans___def_124_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_17 X1 H1) (seval_1_model_auto___def_125 X2 H2))
  end
.
Definition seval_1_model_auto___def_121 (X:term) (pi:(auto___def_121 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_121 X) return (seval_1 X)=val_1_3 with
    (trans___def_121_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_123 X1 H1) (seval_1_model_auto___def_124 X2 H2))
  end
.
Definition seval_1_model_auto___def_120 (X:term) (pi:(auto___def_120 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_120 X) return (seval_1 X)=val_1_5 with
    (trans___def_120_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_121 X1 H1) (seval_1_model_auto___def_122 X2 H2))
  end
.
Definition seval_1_model_auto___def_119 (X:term) (pi:(auto___def_119 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_119 X) return (seval_1 X)=val_1_5 with
    (trans___def_119_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_121 X1 H1) (seval_1_model_auto___def_122 X2 H2))
  end
.
Definition seval_1_model_auto___def_108 (X:term) (pi:(auto___def_108 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_108 X) return (seval_1 X)=val_1_5 with
    (trans___def_108_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_109 X1 H1))
  end
.
Definition seval_1_model_auto___def_69 (X:term) (pi:(auto___def_69 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_69 X) return (seval_1 X)=val_1_5 with
    (trans___def_69_nil_1) => (seval_1_rewrite_nil)
  end
.
Definition seval_1_model_auto___type_9 (X:term) (pi:(auto___type_9 X)):((seval_1 X)=val_1_6) :=
  match pi as pi in (auto___type_9 X) return (seval_1 X)=val_1_6 with
    (trans___type_9_i_1) => (seval_1_rewrite_i)
  | (trans___type_9_bob_1) => (seval_1_rewrite_bob)
  | (trans___type_9_server_1) => (seval_1_rewrite_server)
  | (trans___type_9_alice_1) => (seval_1_rewrite_alice)
  end
.
Definition seval_1_model_auto___type_10 (X:term) (pi:(auto___type_10 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___type_10 X) return (seval_1 X)=val_1_5 with
    (trans___type_10_nonces_old_1 X1 X2 X3 H1 H2 H3) => (seval_1_rewrite_nonces_old (seval_1 X1) (seval_1 X2) (seval_1 X3) val_1_5 val_1_6 val_1_6 (seval_1_model_auto___def_9 X1 H1) (seval_1_model_auto_agent X2 H2) (seval_1_model_auto_agent X3 H3))
  end
.
Definition seval_1_model_auto___def_90 (X:term) (pi:(auto___def_90 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_90 X) return (seval_1 X)=val_1_5 with
    (trans___def_90_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_91 X1 H1))
  end
.
Definition seval_1_model_auto___def_68 (X:term) (pi:(auto___def_68 X)):((seval_1 X)=val_1_9) :=
  match pi as pi in (auto___def_68 X) return (seval_1 X)=val_1_9 with
    (trans___def_68_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_5 (seval_1_model_auto___type_9 X1 H1) (seval_1_model_auto___def_69 X2 H2))
  end
.
Definition seval_1_model_auto___def_67 (X:term) (pi:(auto___def_67 X)):((seval_1 X)=val_1_2) :=
  match pi as pi in (auto___def_67 X) return (seval_1 X)=val_1_2 with
    (trans___def_67_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_6 val_1_9 (seval_1_model_auto___type_11 X1 H1) (seval_1_model_auto___def_68 X2 H2))
  end
.
Definition seval_1_model_auto___def_66 (X:term) (pi:(auto___def_66 X)):((seval_1 X)=val_1_1) :=
  match pi as pi in (auto___def_66 X) return (seval_1 X)=val_1_1 with
    (trans___def_66_sym_1) => (seval_1_rewrite_sym)
  end
.
Definition seval_1_model_auto___def_65 (X:term) (pi:(auto___def_65 X)):((seval_1 X)=val_1_3) :=
  match pi as pi in (auto___def_65 X) return (seval_1 X)=val_1_3 with
    (trans___def_65_key_1 X1 X2 H1 H2) => (seval_1_rewrite_key (seval_1 X1) (seval_1 X2) val_1_1 val_1_2 (seval_1_model_auto___def_66 X1 H1) (seval_1_model_auto___def_67 X2 H2))
  end
.
Definition seval_1_model_auto___def_64 (X:term) (pi:(auto___def_64 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_64 X) return (seval_1 X)=val_1_5 with
    (trans___def_64_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_65 X1 H1) (seval_1_model_auto___type_10 X2 H2))
  end
.
Definition seval_1_model_auto___def_54 (X:term) (pi:(auto___def_54 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_54 X) return (seval_1 X)=val_1_5 with
    (trans___def_54_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  end
.
Definition seval_1_model_auto___def_82 (X:term) (pi:(auto___def_82 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_82 X) return (seval_1 X)=val_1_5 with
    (trans___def_82_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_90 X1 H1) (seval_1_model_auto___def_89 X2 H2))
  end
.
Definition seval_1_model_auto___def_43 (X:term) (pi:(auto___def_43 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_43 X) return (seval_1 X)=val_1_5 with
    (trans___def_43_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_44 X1 H1))
  end
.
Definition seval_1_model_auto___def_25 (X:term) (pi:(auto___def_25 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_25 X) return (seval_1 X)=val_1_5 with
    (trans___def_25_h_1 X1 H1) => (seval_1_rewrite_h (seval_1 X1) val_1_5 (seval_1_model_auto___def_26 X1 H1))
  end
.
Definition seval_1_model_auto___def_63 (X:term) (pi:(auto___def_63 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_63 X) return (seval_1 X)=val_1_5 with
    (trans___def_63_f4_1 X1 X2 H1 H2) => (seval_1_rewrite_f4 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_65 X1 H1) (seval_1_model_auto___type_10 X2 H2))
  end
.
Definition seval_1_model_auto___def_13 (X:term) (pi:(auto___def_13 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_13 X) return (seval_1 X)=val_1_5 with
    (trans___def_13_cons_1 X1 X2 H1 H2) => (seval_1_rewrite_cons (seval_1 X1) (seval_1 X2) val_1_5 val_1_5 (seval_1_model_auto___def_25 X1 H1) (seval_1_model_auto___def_24 X2 H2))
  end
.
Definition seval_1_model_auto___def_55 (X:term) (pi:(auto___def_55 X)):((seval_1 X)=val_1_5) :=
  match pi as pi in (auto___def_55 X) return (seval_1 X)=val_1_5 with
    (trans___def_55_f3_1 X1 X2 H1 H2) => (seval_1_rewrite_f3 (seval_1 X1) (seval_1 X2) val_1_3 val_1_5 (seval_1_model_auto___def_56 X1 H1) (seval_1_model_auto___def_57 X2 H2))
  end
.

Inductive pred : nat -> Set :=
	  pred___type_21 : pred (1)
        | pred___type_20 : pred (1)
	.

Lemma gag : forall X:term, seval_1 t
