\lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
(H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
u2 t2)).(let H_y \def (ty3_sn3 g c u1 t1 H) in (let H_y0 \def (ty3_sn3 g c u2
-t2 H0) in (let H_x \def (nf2_sn3 c u1 H_y) in (let H1 \def H_x in (let TMP_1
-\def (\lambda (u: T).(pr3 c u1 u)) in (let TMP_2 \def (\lambda (u: T).(nf2 c
-u)) in (let TMP_3 \def (pc3 c u1 u2) in (let TMP_4 \def ((pc3 c u1 u2) \to
-False) in (let TMP_5 \def (or TMP_3 TMP_4) in (let TMP_36 \def (\lambda (x:
-T).(\lambda (H2: (pr3 c u1 x)).(\lambda (H3: (nf2 c x)).(let H_x0 \def
-(nf2_sn3 c u2 H_y0) in (let H4 \def H_x0 in (let TMP_6 \def (\lambda (u:
-T).(pr3 c u2 u)) in (let TMP_7 \def (\lambda (u: T).(nf2 c u)) in (let TMP_8
-\def (pc3 c u1 u2) in (let TMP_9 \def ((pc3 c u1 u2) \to False) in (let
-TMP_10 \def (or TMP_8 TMP_9) in (let TMP_35 \def (\lambda (x0: T).(\lambda
+t2 H0) in (let H_x \def (nf2_sn3 c u1 H_y) in (let H1 \def H_x in (ex2_ind T
+(\lambda (u: T).(pr3 c u1 u)) (\lambda (u: T).(nf2 c u)) (or (pc3 c u1 u2)
+((pc3 c u1 u2) \to False)) (\lambda (x: T).(\lambda (H2: (pr3 c u1
+x)).(\lambda (H3: (nf2 c x)).(let H_x0 \def (nf2_sn3 c u2 H_y0) in (let H4
+\def H_x0 in (ex2_ind T (\lambda (u: T).(pr3 c u2 u)) (\lambda (u: T).(nf2 c
+u)) (or (pc3 c u1 u2) ((pc3 c u1 u2) \to False)) (\lambda (x0: T).(\lambda
(H5: (pr3 c u2 x0)).(\lambda (H6: (nf2 c x0)).(let H_x1 \def (term_dec x x0)
-in (let H7 \def H_x1 in (let TMP_11 \def (eq T x x0) in (let TMP_12 \def ((eq
-T x x0) \to (\forall (P: Prop).P)) in (let TMP_13 \def (pc3 c u1 u2) in (let
-TMP_14 \def ((pc3 c u1 u2) \to False) in (let TMP_15 \def (or TMP_13 TMP_14)
-in (let TMP_21 \def (\lambda (H8: (eq T x x0)).(let TMP_16 \def (\lambda (t:
-T).(nf2 c t)) in (let H9 \def (eq_ind_r T x0 TMP_16 H6 x H8) in (let TMP_17
-\def (\lambda (t: T).(pr3 c u2 t)) in (let H10 \def (eq_ind_r T x0 TMP_17 H5
-x H8) in (let TMP_18 \def (pc3 c u1 u2) in (let TMP_19 \def ((pc3 c u1 u2)
-\to False) in (let TMP_20 \def (pc3_pr3_t c u1 x H2 u2 H10) in (or_introl
-TMP_18 TMP_19 TMP_20))))))))) in (let TMP_34 \def (\lambda (H8: (((eq T x x0)
-\to (\forall (P: Prop).P)))).(let TMP_22 \def (pc3 c u1 u2) in (let TMP_23
-\def ((pc3 c u1 u2) \to False) in (let TMP_33 \def (\lambda (H9: (pc3 c u1
-u2)).(let H10 \def H9 in (let TMP_24 \def (\lambda (t: T).(pr3 c u1 t)) in
-(let TMP_25 \def (\lambda (t: T).(pr3 c u2 t)) in (let TMP_32 \def (\lambda
-(x1: T).(\lambda (H11: (pr3 c u1 x1)).(\lambda (H12: (pr3 c u2 x1)).(let H_x2
-\def (pr3_confluence c u2 x0 H5 x1 H12) in (let H13 \def H_x2 in (let TMP_26
-\def (\lambda (t: T).(pr3 c x0 t)) in (let TMP_27 \def (\lambda (t: T).(pr3 c
-x1 t)) in (let TMP_31 \def (\lambda (x2: T).(\lambda (H14: (pr3 c x0
-x2)).(\lambda (H15: (pr3 c x1 x2)).(let H_y1 \def (nf2_pr3_unfold c x0 x2 H14
-H6) in (let TMP_28 \def (\lambda (t: T).(pr3 c x1 t)) in (let H16 \def
-(eq_ind_r T x2 TMP_28 H15 x0 H_y1) in (let H17 \def (nf2_pr3_confluence c x
-H3 x0 H6 u1 H2) in (let TMP_29 \def (pr3_t x1 u1 c H11 x0 H16) in (let TMP_30
-\def (H17 TMP_29) in (H8 TMP_30 False)))))))))) in (ex2_ind T TMP_26 TMP_27
-False TMP_31 H13))))))))) in (ex2_ind T TMP_24 TMP_25 False TMP_32 H10))))))
-in (or_intror TMP_22 TMP_23 TMP_33))))) in (or_ind TMP_11 TMP_12 TMP_15
-TMP_21 TMP_34 H7))))))))))))) in (ex2_ind T TMP_6 TMP_7 TMP_10 TMP_35
-H4)))))))))))) in (ex2_ind T TMP_1 TMP_2 TMP_5 TMP_36 H1)))))))))))))))))).
+in (let H7 \def H_x1 in (or_ind (eq T x x0) ((eq T x x0) \to (\forall (P:
+Prop).P)) (or (pc3 c u1 u2) ((pc3 c u1 u2) \to False)) (\lambda (H8: (eq T x
+x0)).(let H9 \def (eq_ind_r T x0 (\lambda (t: T).(nf2 c t)) H6 x H8) in (let
+H10 \def (eq_ind_r T x0 (\lambda (t: T).(pr3 c u2 t)) H5 x H8) in (or_introl
+(pc3 c u1 u2) ((pc3 c u1 u2) \to False) (pc3_pr3_t c u1 x H2 u2 H10)))))
+(\lambda (H8: (((eq T x x0) \to (\forall (P: Prop).P)))).(or_intror (pc3 c u1
+u2) ((pc3 c u1 u2) \to False) (\lambda (H9: (pc3 c u1 u2)).(let H10 \def H9
+in (ex2_ind T (\lambda (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t))
+False (\lambda (x1: T).(\lambda (H11: (pr3 c u1 x1)).(\lambda (H12: (pr3 c u2
+x1)).(let H_x2 \def (pr3_confluence c u2 x0 H5 x1 H12) in (let H13 \def H_x2
+in (ex2_ind T (\lambda (t: T).(pr3 c x0 t)) (\lambda (t: T).(pr3 c x1 t))
+False (\lambda (x2: T).(\lambda (H14: (pr3 c x0 x2)).(\lambda (H15: (pr3 c x1
+x2)).(let H_y1 \def (nf2_pr3_unfold c x0 x2 H14 H6) in (let H16 \def
+(eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def
+(nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0
+H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
theorem pc3_abst_dec:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
\lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
(H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
u2 t2)).(let H1 \def (ty3_sn3 g c u1 t1 H) in (let H2 \def (ty3_sn3 g c u2 t2
-H0) in (let H_x \def (nf2_sn3 c u1 H1) in (let H3 \def H_x in (let TMP_1 \def
-(\lambda (u: T).(pr3 c u1 u)) in (let TMP_2 \def (\lambda (u: T).(nf2 c u))
-in (let TMP_5 \def (\lambda (u: T).(\lambda (_: T).(let TMP_3 \def (Bind
-Abst) in (let TMP_4 \def (THead TMP_3 u2 u) in (pc3 c u1 TMP_4))))) in (let
-TMP_8 \def (\lambda (u: T).(\lambda (v2: T).(let TMP_6 \def (Bind Abst) in
-(let TMP_7 \def (THead TMP_6 v2 u) in (ty3 g c TMP_7 t1))))) in (let TMP_9
-\def (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) in (let TMP_10 \def
-(\lambda (_: T).(\lambda (v2: T).(nf2 c v2))) in (let TMP_11 \def (ex4_2 T T
-TMP_5 TMP_8 TMP_9 TMP_10) in (let TMP_12 \def (\forall (u: T).((pc3 c u1
-(THead (Bind Abst) u2 u)) \to False)) in (let TMP_13 \def (or TMP_11 TMP_12)
-in (let TMP_162 \def (\lambda (x: T).(\lambda (H4: (pr3 c u1 x)).(\lambda
-(H5: (nf2 c x)).(let H_x0 \def (nf2_sn3 c u2 H2) in (let H6 \def H_x0 in (let
-TMP_14 \def (\lambda (u: T).(pr3 c u2 u)) in (let TMP_15 \def (\lambda (u:
-T).(nf2 c u)) in (let TMP_18 \def (\lambda (u: T).(\lambda (_: T).(let TMP_16
-\def (Bind Abst) in (let TMP_17 \def (THead TMP_16 u2 u) in (pc3 c u1
-TMP_17))))) in (let TMP_21 \def (\lambda (u: T).(\lambda (v2: T).(let TMP_19
-\def (Bind Abst) in (let TMP_20 \def (THead TMP_19 v2 u) in (ty3 g c TMP_20
-t1))))) in (let TMP_22 \def (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2)))
-in (let TMP_23 \def (\lambda (_: T).(\lambda (v2: T).(nf2 c v2))) in (let
-TMP_24 \def (ex4_2 T T TMP_18 TMP_21 TMP_22 TMP_23) in (let TMP_25 \def
-(\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u)) \to False)) in (let
-TMP_26 \def (or TMP_24 TMP_25) in (let TMP_161 \def (\lambda (x0: T).(\lambda
-(H7: (pr3 c u2 x0)).(\lambda (H8: (nf2 c x0)).(let H_x1 \def (abst_dec x x0)
-in (let H9 \def H_x1 in (let TMP_29 \def (\lambda (t: T).(let TMP_27 \def
-(Bind Abst) in (let TMP_28 \def (THead TMP_27 x0 t) in (eq T x TMP_28)))) in
-(let TMP_30 \def (ex T TMP_29) in (let TMP_31 \def (\forall (t: T).((eq T x
-(THead (Bind Abst) x0 t)) \to (\forall (P: Prop).P))) in (let TMP_34 \def
-(\lambda (u: T).(\lambda (_: T).(let TMP_32 \def (Bind Abst) in (let TMP_33
-\def (THead TMP_32 u2 u) in (pc3 c u1 TMP_33))))) in (let TMP_37 \def
-(\lambda (u: T).(\lambda (v2: T).(let TMP_35 \def (Bind Abst) in (let TMP_36
-\def (THead TMP_35 v2 u) in (ty3 g c TMP_36 t1))))) in (let TMP_38 \def
-(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) in (let TMP_39 \def (\lambda
-(_: T).(\lambda (v2: T).(nf2 c v2))) in (let TMP_40 \def (ex4_2 T T TMP_34
-TMP_37 TMP_38 TMP_39) in (let TMP_41 \def (\forall (u: T).((pc3 c u1 (THead
-(Bind Abst) u2 u)) \to False)) in (let TMP_42 \def (or TMP_40 TMP_41) in (let
-TMP_95 \def (\lambda (H10: (ex T (\lambda (t: T).(eq T x (THead (Bind Abst)
-x0 t))))).(let TMP_45 \def (\lambda (t: T).(let TMP_43 \def (Bind Abst) in
-(let TMP_44 \def (THead TMP_43 x0 t) in (eq T x TMP_44)))) in (let TMP_48
-\def (\lambda (u: T).(\lambda (_: T).(let TMP_46 \def (Bind Abst) in (let
-TMP_47 \def (THead TMP_46 u2 u) in (pc3 c u1 TMP_47))))) in (let TMP_51 \def
-(\lambda (u: T).(\lambda (v2: T).(let TMP_49 \def (Bind Abst) in (let TMP_50
-\def (THead TMP_49 v2 u) in (ty3 g c TMP_50 t1))))) in (let TMP_52 \def
-(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) in (let TMP_53 \def (\lambda
-(_: T).(\lambda (v2: T).(nf2 c v2))) in (let TMP_54 \def (ex4_2 T T TMP_48
-TMP_51 TMP_52 TMP_53) in (let TMP_55 \def (\forall (u: T).((pc3 c u1 (THead
-(Bind Abst) u2 u)) \to False)) in (let TMP_56 \def (or TMP_54 TMP_55) in (let
-TMP_94 \def (\lambda (x1: T).(\lambda (H11: (eq T x (THead (Bind Abst) x0
-x1))).(let TMP_57 \def (\lambda (t: T).(nf2 c t)) in (let TMP_58 \def (Bind
-Abst) in (let TMP_59 \def (THead TMP_58 x0 x1) in (let H12 \def (eq_ind T x
-TMP_57 H5 TMP_59 H11) in (let TMP_60 \def (\lambda (t: T).(pr3 c u1 t)) in
-(let TMP_61 \def (Bind Abst) in (let TMP_62 \def (THead TMP_61 x0 x1) in (let
-H13 \def (eq_ind T x TMP_60 H4 TMP_62 H11) in (let TMP_63 \def (Bind Abst) in
-(let TMP_64 \def (THead TMP_63 x0 x1) in (let H_y \def (ty3_sred_pr3 c u1
-TMP_64 H13 g t1 H) in (let TMP_67 \def (\lambda (u: T).(\lambda (_: T).(let
-TMP_65 \def (Bind Abst) in (let TMP_66 \def (THead TMP_65 u2 u) in (pc3 c u1
-TMP_66))))) in (let TMP_70 \def (\lambda (u: T).(\lambda (v2: T).(let TMP_68
-\def (Bind Abst) in (let TMP_69 \def (THead TMP_68 v2 u) in (ty3 g c TMP_69
-t1))))) in (let TMP_71 \def (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2)))
-in (let TMP_72 \def (\lambda (_: T).(\lambda (v2: T).(nf2 c v2))) in (let
-TMP_73 \def (ex4_2 T T TMP_67 TMP_70 TMP_71 TMP_72) in (let TMP_74 \def
-(\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u)) \to False)) in (let
-TMP_77 \def (\lambda (u: T).(\lambda (_: T).(let TMP_75 \def (Bind Abst) in
-(let TMP_76 \def (THead TMP_75 u2 u) in (pc3 c u1 TMP_76))))) in (let TMP_80
-\def (\lambda (u: T).(\lambda (v2: T).(let TMP_78 \def (Bind Abst) in (let
-TMP_79 \def (THead TMP_78 v2 u) in (ty3 g c TMP_79 t1))))) in (let TMP_81
-\def (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) in (let TMP_82 \def
-(\lambda (_: T).(\lambda (v2: T).(nf2 c v2))) in (let TMP_83 \def (Bind Abst)
-in (let TMP_84 \def (THead TMP_83 x0 x1) in (let TMP_85 \def (Bind Abst) in
-(let TMP_86 \def (THead TMP_85 u2 x1) in (let TMP_87 \def (Bind Abst) in (let
-TMP_88 \def (Bind Abst) in (let TMP_89 \def (CHead c TMP_88 x0) in (let
-TMP_90 \def (pr3_refl TMP_89 x1) in (let TMP_91 \def (pr3_head_12 c u2 x0 H7
-TMP_87 x1 x1 TMP_90) in (let TMP_92 \def (pc3_pr3_t c u1 TMP_84 H13 TMP_86
-TMP_91) in (let TMP_93 \def (ex4_2_intro T T TMP_77 TMP_80 TMP_81 TMP_82 x1
-x0 TMP_92 H_y H7 H8) in (or_introl TMP_73 TMP_74
-TMP_93))))))))))))))))))))))))))))))))))) in (ex_ind T TMP_45 TMP_56 TMP_94
-H10))))))))))) in (let TMP_160 \def (\lambda (H10: ((\forall (t: T).((eq T x
-(THead (Bind Abst) x0 t)) \to (\forall (P: Prop).P))))).(let TMP_98 \def
-(\lambda (u: T).(\lambda (_: T).(let TMP_96 \def (Bind Abst) in (let TMP_97
-\def (THead TMP_96 u2 u) in (pc3 c u1 TMP_97))))) in (let TMP_101 \def
-(\lambda (u: T).(\lambda (v2: T).(let TMP_99 \def (Bind Abst) in (let TMP_100
-\def (THead TMP_99 v2 u) in (ty3 g c TMP_100 t1))))) in (let TMP_102 \def
-(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) in (let TMP_103 \def
-(\lambda (_: T).(\lambda (v2: T).(nf2 c v2))) in (let TMP_104 \def (ex4_2 T T
-TMP_98 TMP_101 TMP_102 TMP_103) in (let TMP_105 \def (\forall (u: T).((pc3 c
-u1 (THead (Bind Abst) u2 u)) \to False)) in (let TMP_159 \def (\lambda (u:
-T).(\lambda (H11: (pc3 c u1 (THead (Bind Abst) u2 u))).(let H12 \def H11 in
-(let TMP_106 \def (\lambda (t: T).(pr3 c u1 t)) in (let TMP_109 \def (\lambda
-(t: T).(let TMP_107 \def (Bind Abst) in (let TMP_108 \def (THead TMP_107 u2
-u) in (pr3 c TMP_108 t)))) in (let TMP_158 \def (\lambda (x1: T).(\lambda
-(H13: (pr3 c u1 x1)).(\lambda (H14: (pr3 c (THead (Bind Abst) u2 u) x1)).(let
-TMP_110 \def (\lambda (t: T).(pr3 c x1 t)) in (let TMP_111 \def (\lambda (t:
-T).(pr3 c x t)) in (let TMP_156 \def (\lambda (x2: T).(\lambda (H15: (pr3 c
-x1 x2)).(\lambda (H16: (pr3 c x x2)).(let H_y \def (nf2_pr3_unfold c x x2 H16
-H5) in (let TMP_112 \def (\lambda (t: T).(pr3 c x1 t)) in (let H17 \def
-(eq_ind_r T x2 TMP_112 H15 x H_y) in (let H18 \def (pr3_gen_abst c u2 u x1
-H14) in (let TMP_115 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_113 \def
-(Bind Abst) in (let TMP_114 \def (THead TMP_113 u3 t3) in (eq T x1
-TMP_114))))) in (let TMP_116 \def (\lambda (u3: T).(\lambda (_: T).(pr3 c u2
-u3))) in (let TMP_119 \def (\lambda (_: T).(\lambda (t3: T).(\forall (b:
-B).(\forall (u0: T).(let TMP_117 \def (Bind b) in (let TMP_118 \def (CHead c
-TMP_117 u0) in (pr3 TMP_118 u t3))))))) in (let TMP_155 \def (\lambda (x3:
-T).(\lambda (x4: T).(\lambda (H19: (eq T x1 (THead (Bind Abst) x3
-x4))).(\lambda (H20: (pr3 c u2 x3)).(\lambda (_: ((\forall (b: B).(\forall
-(u0: T).(pr3 (CHead c (Bind b) u0) u x4))))).(let TMP_120 \def (\lambda (t:
-T).(pr3 c t x)) in (let TMP_121 \def (Bind Abst) in (let TMP_122 \def (THead
-TMP_121 x3 x4) in (let H22 \def (eq_ind T x1 TMP_120 H17 TMP_122 H19) in (let
-H23 \def (pr3_gen_abst c x3 x4 x H22) in (let TMP_125 \def (\lambda (u3:
-T).(\lambda (t3: T).(let TMP_123 \def (Bind Abst) in (let TMP_124 \def (THead
-TMP_123 u3 t3) in (eq T x TMP_124))))) in (let TMP_126 \def (\lambda (u3:
-T).(\lambda (_: T).(pr3 c x3 u3))) in (let TMP_129 \def (\lambda (_:
-T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(let TMP_127 \def (Bind
-b) in (let TMP_128 \def (CHead c TMP_127 u0) in (pr3 TMP_128 x4 t3))))))) in
-(let TMP_154 \def (\lambda (x5: T).(\lambda (x6: T).(\lambda (H24: (eq T x
-(THead (Bind Abst) x5 x6))).(\lambda (H25: (pr3 c x3 x5)).(\lambda (_:
-((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b) u0) x4 x6))))).(let
-TMP_130 \def (\lambda (t: T).(\forall (t0: T).((eq T t (THead (Bind Abst) x0
-t0)) \to (\forall (P: Prop).P)))) in (let TMP_131 \def (Bind Abst) in (let
-TMP_132 \def (THead TMP_131 x5 x6) in (let H27 \def (eq_ind T x TMP_130 H10
-TMP_132 H24) in (let TMP_133 \def (\lambda (t: T).(nf2 c t)) in (let TMP_134
-\def (Bind Abst) in (let TMP_135 \def (THead TMP_134 x5 x6) in (let H28 \def
-(eq_ind T x TMP_133 H5 TMP_135 H24) in (let H29 \def (nf2_gen_abst c x5 x6
-H28) in (let TMP_136 \def (nf2 c x5) in (let TMP_137 \def (Bind Abst) in (let
-TMP_138 \def (CHead c TMP_137 x5) in (let TMP_139 \def (nf2 TMP_138 x6) in
-(let TMP_153 \def (\lambda (H30: (nf2 c x5)).(\lambda (_: (nf2 (CHead c (Bind
+H0) in (let H_x \def (nf2_sn3 c u1 H1) in (let H3 \def H_x in (ex2_ind T
+(\lambda (u: T).(pr3 c u1 u)) (\lambda (u: T).(nf2 c u)) (or (ex4_2 T T
+(\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
+(\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
+(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
+(v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
+\to False))) (\lambda (x: T).(\lambda (H4: (pr3 c u1 x)).(\lambda (H5: (nf2 c
+x)).(let H_x0 \def (nf2_sn3 c u2 H2) in (let H6 \def H_x0 in (ex2_ind T
+(\lambda (u: T).(pr3 c u2 u)) (\lambda (u: T).(nf2 c u)) (or (ex4_2 T T
+(\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
+(\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
+(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
+(v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
+\to False))) (\lambda (x0: T).(\lambda (H7: (pr3 c u2 x0)).(\lambda (H8: (nf2
+c x0)).(let H_x1 \def (abst_dec x x0) in (let H9 \def H_x1 in (or_ind (ex T
+(\lambda (t: T).(eq T x (THead (Bind Abst) x0 t)))) (\forall (t: T).((eq T x
+(THead (Bind Abst) x0 t)) \to (\forall (P: Prop).P))) (or (ex4_2 T T (\lambda
+(u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u)))) (\lambda (u:
+T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1))) (\lambda (_:
+T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda (v2: T).(nf2 c
+v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u)) \to False)))
+(\lambda (H10: (ex T (\lambda (t: T).(eq T x (THead (Bind Abst) x0
+t))))).(ex_ind T (\lambda (t: T).(eq T x (THead (Bind Abst) x0 t))) (or
+(ex4_2 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2
+u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u)
+t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_:
+T).(\lambda (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind
+Abst) u2 u)) \to False))) (\lambda (x1: T).(\lambda (H11: (eq T x (THead
+(Bind Abst) x0 x1))).(let H12 \def (eq_ind T x (\lambda (t: T).(nf2 c t)) H5
+(THead (Bind Abst) x0 x1) H11) in (let H13 \def (eq_ind T x (\lambda (t:
+T).(pr3 c u1 t)) H4 (THead (Bind Abst) x0 x1) H11) in (let H_y \def
+(ty3_sred_pr3 c u1 (THead (Bind Abst) x0 x1) H13 g t1 H) in (or_introl (ex4_2
+T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
+(\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
+(\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
+(v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
+\to False)) (ex4_2_intro T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead
+(Bind Abst) u2 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind
+Abst) v2 u) t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda
+(_: T).(\lambda (v2: T).(nf2 c v2))) x1 x0 (pc3_pr3_t c u1 (THead (Bind Abst)
+x0 x1) H13 (THead (Bind Abst) u2 x1) (pr3_head_12 c u2 x0 H7 (Bind Abst) x1
+x1 (pr3_refl (CHead c (Bind Abst) x0) x1))) H_y H7 H8))))))) H10)) (\lambda
+(H10: ((\forall (t: T).((eq T x (THead (Bind Abst) x0 t)) \to (\forall (P:
+Prop).P))))).(or_intror (ex4_2 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1
+(THead (Bind Abst) u2 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead
+(Bind Abst) v2 u) t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2)))
+(\lambda (_: T).(\lambda (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1
+(THead (Bind Abst) u2 u)) \to False)) (\lambda (u: T).(\lambda (H11: (pc3 c
+u1 (THead (Bind Abst) u2 u))).(let H12 \def H11 in (ex2_ind T (\lambda (t:
+T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 u) t)) False
+(\lambda (x1: T).(\lambda (H13: (pr3 c u1 x1)).(\lambda (H14: (pr3 c (THead
+(Bind Abst) u2 u) x1)).(ex2_ind T (\lambda (t: T).(pr3 c x1 t)) (\lambda (t:
+T).(pr3 c x t)) False (\lambda (x2: T).(\lambda (H15: (pr3 c x1 x2)).(\lambda
+(H16: (pr3 c x x2)).(let H_y \def (nf2_pr3_unfold c x x2 H16 H5) in (let H17
+\def (eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x H_y) in (let H18 \def
+(pr3_gen_abst c u2 u x1 H14) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3:
+T).(eq T x1 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_:
+T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
+(u0: T).(pr3 (CHead c (Bind b) u0) u t3))))) False (\lambda (x3: T).(\lambda
+(x4: T).(\lambda (H19: (eq T x1 (THead (Bind Abst) x3 x4))).(\lambda (H20:
+(pr3 c u2 x3)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c
+(Bind b) u0) u x4))))).(let H22 \def (eq_ind T x1 (\lambda (t: T).(pr3 c t
+x)) H17 (THead (Bind Abst) x3 x4) H19) in (let H23 \def (pr3_gen_abst c x3 x4
+x H22) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
+(Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c x3 u3)))
+(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead
+c (Bind b) u0) x4 t3))))) False (\lambda (x5: T).(\lambda (x6: T).(\lambda
+(H24: (eq T x (THead (Bind Abst) x5 x6))).(\lambda (H25: (pr3 c x3
+x5)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
+u0) x4 x6))))).(let H27 \def (eq_ind T x (\lambda (t: T).(\forall (t0:
+T).((eq T t (THead (Bind Abst) x0 t0)) \to (\forall (P: Prop).P)))) H10
+(THead (Bind Abst) x5 x6) H24) in (let H28 \def (eq_ind T x (\lambda (t:
+T).(nf2 c t)) H5 (THead (Bind Abst) x5 x6) H24) in (let H29 \def
+(nf2_gen_abst c x5 x6 H28) in (land_ind (nf2 c x5) (nf2 (CHead c (Bind Abst)
+x5) x6) False (\lambda (H30: (nf2 c x5)).(\lambda (_: (nf2 (CHead c (Bind
Abst) x5) x6)).(let H32 \def (nf2_pr3_confluence c x0 H8 x5 H30 u2 H7) in
-(let TMP_140 \def (Bind Abst) in (let TMP_141 \def (THead TMP_140 x0 x6) in
-(let TMP_142 \def (Bind Abst) in (let TMP_143 \def (THead TMP_142 x5 x6) in
-(let TMP_144 \def (Bind Abst) in (let TMP_145 \def (Bind Abst) in (let
-TMP_146 \def (Bind Abst) in (let TMP_147 \def (refl_equal K TMP_146) in (let
-TMP_148 \def (pr3_t x3 u2 c H20 x5 H25) in (let TMP_149 \def (H32 TMP_148) in
-(let TMP_150 \def (refl_equal T x6) in (let TMP_151 \def (f_equal3 K T T T
-THead TMP_144 TMP_145 x0 x5 x6 x6 TMP_147 TMP_149 TMP_150) in (let TMP_152
-\def (sym_eq T TMP_141 TMP_143 TMP_151) in (H27 x6 TMP_152
-False))))))))))))))))) in (land_ind TMP_136 TMP_139 False TMP_153
-H29)))))))))))))))))))) in (ex3_2_ind T T TMP_125 TMP_126 TMP_129 False
-TMP_154 H23))))))))))))))) in (ex3_2_ind T T TMP_115 TMP_116 TMP_119 False
-TMP_155 H18)))))))))))) in (let TMP_157 \def (pr3_confluence c u1 x1 H13 x
-H4) in (ex2_ind T TMP_110 TMP_111 False TMP_156 TMP_157)))))))) in (ex2_ind T
-TMP_106 TMP_109 False TMP_158 H12))))))) in (or_intror TMP_104 TMP_105
-TMP_159))))))))) in (or_ind TMP_30 TMP_31 TMP_42 TMP_95 TMP_160
-H9)))))))))))))))))) in (ex2_ind T TMP_14 TMP_15 TMP_26 TMP_161
-H6)))))))))))))))) in (ex2_ind T TMP_1 TMP_2 TMP_13 TMP_162
-H3)))))))))))))))))))))).
+(H27 x6 (sym_eq T (THead (Bind Abst) x0 x6) (THead (Bind Abst) x5 x6)
+(f_equal3 K T T T THead (Bind Abst) (Bind Abst) x0 x5 x6 x6 (refl_equal K
+(Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False))))
+H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4)))))
+H12)))))) H9)))))) H6)))))) H3)))))))))))).
projects / helm.git / blobdiff