-(H3: (pr0 t0 t4)).(\lambda (H4: (subst0 i0 u0 t4 t2)).(ex2_ind T (\lambda (t:
-T).(pr0 t4 t)) (\lambda (t: T).(pr0 t3 t)) (ex2 T (\lambda (t: T).(pr2 c t1
-t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x: T).(\lambda (H5: (pr0 t4
-x)).(\lambda (H6: (pr0 t3 x)).(or_ind (pr0 t1 x) (ex2 T (\lambda (w2: T).(pr0
-t1 w2)) (\lambda (w2: T).(subst0 i u x w2))) (ex2 T (\lambda (t: T).(pr2 c t1
-t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H7: (pr0 t1 x)).(or_ind (pr0 t2
-x) (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
-w2))) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
-(\lambda (H8: (pr0 t2 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda
-(t: T).(pr2 c t2 t)) x (pr2_free c t1 x H7) (pr2_free c t2 x H8))) (\lambda
-(H8: (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
-w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0
-u0 x w2)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
-(\lambda (x0: T).(\lambda (H9: (pr0 t2 x0)).(\lambda (H10: (subst0 i0 u0 x
-x0)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))
-x0 (pr2_delta c d0 u0 i0 H2 t1 x H7 x0 H10) (pr2_free c t2 x0 H9))))) H8))
-(pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))) (\lambda (H7: (ex2 T
-(\lambda (w2: T).(pr0 t1 w2)) (\lambda (w2: T).(subst0 i u x w2)))).(ex2_ind
-T (\lambda (w2: T).(pr0 t1 w2)) (\lambda (w2: T).(subst0 i u x w2)) (ex2 T
-(\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x0:
-T).(\lambda (H8: (pr0 t1 x0)).(\lambda (H9: (subst0 i u x x0)).(or_ind (pr0
-t2 x) (ex2 T (\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x
-w2))) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
-(\lambda (H10: (pr0 t2 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t))
-(\lambda (t: T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_delta c d u i H
-t2 x H10 x0 H9))) (\lambda (H10: (ex2 T (\lambda (w2: T).(pr0 t2 w2))
-(\lambda (w2: T).(subst0 i0 u0 x w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t2
-w2)) (\lambda (w2: T).(subst0 i0 u0 x w2)) (ex2 T (\lambda (t: T).(pr2 c t1
-t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (x1: T).(\lambda (H11: (pr0 t2
-x1)).(\lambda (H12: (subst0 i0 u0 x x1)).(neq_eq_e i i0 (ex2 T (\lambda (t:
-T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H13: (not (eq nat i
-i0))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0
-i0 u0 x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
-t))) (\lambda (x2: T).(\lambda (H14: (subst0 i u x1 x2)).(\lambda (H15:
-(subst0 i0 u0 x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
-T).(pr2 c t2 t)) x2 (pr2_delta c d0 u0 i0 H2 t1 x0 H8 x2 H15) (pr2_delta c d
-u i H t2 x1 H11 x2 H14))))) (subst0_confluence_neq x x1 u0 i0 H12 x0 u i H9
-(sym_not_eq nat i i0 H13)))) (\lambda (H13: (eq nat i i0)).(let H14 \def
-(eq_ind_r nat i0 (\lambda (n: nat).(subst0 n u0 x x1)) H12 i H13) in (let H15
-\def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d0 (Bind Abbr) u0)))
-H2 i H13) in (let H16 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0:
-C).(getl i c c0)) H (CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind
-Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (let H17 \def (f_equal C C
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u)
-(CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0
-(Bind Abbr) u0) H15)) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e
-in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
-\Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0) (getl_mono
-c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (\lambda
-(H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0 (\lambda (t: T).(subst0 i t x
-x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0 (\lambda (t: T).(getl i c
-(CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22 \def (eq_ind_r C d0
-(\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21 d H19) in (or4_ind
-(eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t:
-T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1) (ex2 T (\lambda
-(t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H23: (eq T x1
-x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t)) H11 x0 H23) in
-(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0
-(pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda (H23: (ex2 T
-(\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u x0
-t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i
-u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
+(H3: (pr0 t0 t4)).(\lambda (H4: (subst0 i0 u0 t4 t2)).(let TMP_1 \def
+(\lambda (t: T).(pr0 t4 t)) in (let TMP_2 \def (\lambda (t: T).(pr0 t3 t)) in
+(let TMP_3 \def (\lambda (t: T).(pr2 c t1 t)) in (let TMP_4 \def (\lambda (t:
+T).(pr2 c t2 t)) in (let TMP_5 \def (ex2 T TMP_3 TMP_4) in (let TMP_165 \def
+(\lambda (x: T).(\lambda (H5: (pr0 t4 x)).(\lambda (H6: (pr0 t3 x)).(let
+TMP_6 \def (pr0 t1 x) in (let TMP_7 \def (\lambda (w2: T).(pr0 t1 w2)) in
+(let TMP_8 \def (\lambda (w2: T).(subst0 i u x w2)) in (let TMP_9 \def (ex2 T
+TMP_7 TMP_8) in (let TMP_10 \def (\lambda (t: T).(pr2 c t1 t)) in (let TMP_11
+\def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_12 \def (ex2 T TMP_10 TMP_11)
+in (let TMP_38 \def (\lambda (H7: (pr0 t1 x)).(let TMP_13 \def (pr0 t2 x) in
+(let TMP_14 \def (\lambda (w2: T).(pr0 t2 w2)) in (let TMP_15 \def (\lambda
+(w2: T).(subst0 i0 u0 x w2)) in (let TMP_16 \def (ex2 T TMP_14 TMP_15) in
+(let TMP_17 \def (\lambda (t: T).(pr2 c t1 t)) in (let TMP_18 \def (\lambda
+(t: T).(pr2 c t2 t)) in (let TMP_19 \def (ex2 T TMP_17 TMP_18) in (let TMP_24
+\def (\lambda (H8: (pr0 t2 x)).(let TMP_20 \def (\lambda (t: T).(pr2 c t1 t))
+in (let TMP_21 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_22 \def
+(pr2_free c t1 x H7) in (let TMP_23 \def (pr2_free c t2 x H8) in (ex_intro2 T
+TMP_20 TMP_21 x TMP_22 TMP_23)))))) in (let TMP_35 \def (\lambda (H8: (ex2 T
+(\lambda (w2: T).(pr0 t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x w2)))).(let
+TMP_25 \def (\lambda (w2: T).(pr0 t2 w2)) in (let TMP_26 \def (\lambda (w2:
+T).(subst0 i0 u0 x w2)) in (let TMP_27 \def (\lambda (t: T).(pr2 c t1 t)) in
+(let TMP_28 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_29 \def (ex2 T
+TMP_27 TMP_28) in (let TMP_34 \def (\lambda (x0: T).(\lambda (H9: (pr0 t2
+x0)).(\lambda (H10: (subst0 i0 u0 x x0)).(let TMP_30 \def (\lambda (t:
+T).(pr2 c t1 t)) in (let TMP_31 \def (\lambda (t: T).(pr2 c t2 t)) in (let
+TMP_32 \def (pr2_delta c d0 u0 i0 H2 t1 x H7 x0 H10) in (let TMP_33 \def
+(pr2_free c t2 x0 H9) in (ex_intro2 T TMP_30 TMP_31 x0 TMP_32 TMP_33))))))))
+in (ex2_ind T TMP_25 TMP_26 TMP_29 TMP_34 H8)))))))) in (let TMP_36 \def
+(pr0_refl u0) in (let TMP_37 \def (pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 TMP_36)
+in (or_ind TMP_13 TMP_16 TMP_19 TMP_24 TMP_35 TMP_37))))))))))))) in (let
+TMP_162 \def (\lambda (H7: (ex2 T (\lambda (w2: T).(pr0 t1 w2)) (\lambda (w2:
+T).(subst0 i u x w2)))).(let TMP_39 \def (\lambda (w2: T).(pr0 t1 w2)) in
+(let TMP_40 \def (\lambda (w2: T).(subst0 i u x w2)) in (let TMP_41 \def
+(\lambda (t: T).(pr2 c t1 t)) in (let TMP_42 \def (\lambda (t: T).(pr2 c t2
+t)) in (let TMP_43 \def (ex2 T TMP_41 TMP_42) in (let TMP_161 \def (\lambda
+(x0: T).(\lambda (H8: (pr0 t1 x0)).(\lambda (H9: (subst0 i u x x0)).(let
+TMP_44 \def (pr0 t2 x) in (let TMP_45 \def (\lambda (w2: T).(pr0 t2 w2)) in
+(let TMP_46 \def (\lambda (w2: T).(subst0 i0 u0 x w2)) in (let TMP_47 \def
+(ex2 T TMP_45 TMP_46) in (let TMP_48 \def (\lambda (t: T).(pr2 c t1 t)) in
+(let TMP_49 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_50 \def (ex2 T
+TMP_48 TMP_49) in (let TMP_55 \def (\lambda (H10: (pr0 t2 x)).(let TMP_51
+\def (\lambda (t: T).(pr2 c t1 t)) in (let TMP_52 \def (\lambda (t: T).(pr2 c
+t2 t)) in (let TMP_53 \def (pr2_free c t1 x0 H8) in (let TMP_54 \def
+(pr2_delta c d u i H t2 x H10 x0 H9) in (ex_intro2 T TMP_51 TMP_52 x0 TMP_53
+TMP_54)))))) in (let TMP_158 \def (\lambda (H10: (ex2 T (\lambda (w2: T).(pr0
+t2 w2)) (\lambda (w2: T).(subst0 i0 u0 x w2)))).(let TMP_56 \def (\lambda
+(w2: T).(pr0 t2 w2)) in (let TMP_57 \def (\lambda (w2: T).(subst0 i0 u0 x
+w2)) in (let TMP_58 \def (\lambda (t: T).(pr2 c t1 t)) in (let TMP_59 \def
+(\lambda (t: T).(pr2 c t2 t)) in (let TMP_60 \def (ex2 T TMP_58 TMP_59) in
+(let TMP_157 \def (\lambda (x1: T).(\lambda (H11: (pr0 t2 x1)).(\lambda (H12:
+(subst0 i0 u0 x x1)).(let TMP_61 \def (\lambda (t: T).(pr2 c t1 t)) in (let
+TMP_62 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_63 \def (ex2 T TMP_61
+TMP_62) in (let TMP_76 \def (\lambda (H13: (not (eq nat i i0))).(let TMP_64
+\def (\lambda (t: T).(subst0 i u x1 t)) in (let TMP_65 \def (\lambda (t:
+T).(subst0 i0 u0 x0 t)) in (let TMP_66 \def (\lambda (t: T).(pr2 c t1 t)) in
+(let TMP_67 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_68 \def (ex2 T
+TMP_66 TMP_67) in (let TMP_73 \def (\lambda (x2: T).(\lambda (H14: (subst0 i
+u x1 x2)).(\lambda (H15: (subst0 i0 u0 x0 x2)).(let TMP_69 \def (\lambda (t:
+T).(pr2 c t1 t)) in (let TMP_70 \def (\lambda (t: T).(pr2 c t2 t)) in (let
+TMP_71 \def (pr2_delta c d0 u0 i0 H2 t1 x0 H8 x2 H15) in (let TMP_72 \def
+(pr2_delta c d u i H t2 x1 H11 x2 H14) in (ex_intro2 T TMP_69 TMP_70 x2
+TMP_71 TMP_72)))))))) in (let TMP_74 \def (sym_not_eq nat i i0 H13) in (let
+TMP_75 \def (subst0_confluence_neq x x1 u0 i0 H12 x0 u i H9 TMP_74) in
+(ex2_ind T TMP_64 TMP_65 TMP_68 TMP_73 TMP_75)))))))))) in (let TMP_156 \def
+(\lambda (H13: (eq nat i i0)).(let TMP_77 \def (\lambda (n: nat).(subst0 n u0
+x x1)) in (let H14 \def (eq_ind_r nat i0 TMP_77 H12 i H13) in (let TMP_80
+\def (\lambda (n: nat).(let TMP_78 \def (Bind Abbr) in (let TMP_79 \def
+(CHead d0 TMP_78 u0) in (getl n c TMP_79)))) in (let H15 \def (eq_ind_r nat
+i0 TMP_80 H2 i H13) in (let TMP_81 \def (Bind Abbr) in (let TMP_82 \def
+(CHead d TMP_81 u) in (let TMP_83 \def (\lambda (c0: C).(getl i c c0)) in
+(let TMP_84 \def (Bind Abbr) in (let TMP_85 \def (CHead d0 TMP_84 u0) in (let
+TMP_86 \def (Bind Abbr) in (let TMP_87 \def (CHead d TMP_86 u) in (let TMP_88
+\def (Bind Abbr) in (let TMP_89 \def (CHead d0 TMP_88 u0) in (let TMP_90 \def
+(getl_mono c TMP_87 i H TMP_89 H15) in (let H16 \def (eq_ind C TMP_82 TMP_83
+H TMP_85 TMP_90) in (let TMP_91 \def (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_92 \def (Bind
+Abbr) in (let TMP_93 \def (CHead d TMP_92 u) in (let TMP_94 \def (Bind Abbr)
+in (let TMP_95 \def (CHead d0 TMP_94 u0) in (let TMP_96 \def (Bind Abbr) in
+(let TMP_97 \def (CHead d TMP_96 u) in (let TMP_98 \def (Bind Abbr) in (let
+TMP_99 \def (CHead d0 TMP_98 u0) in (let TMP_100 \def (getl_mono c TMP_97 i H
+TMP_99 H15) in (let H17 \def (f_equal C C TMP_91 TMP_93 TMP_95 TMP_100) in
+(let TMP_101 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u |
+(CHead _ _ t) \Rightarrow t])) in (let TMP_102 \def (Bind Abbr) in (let
+TMP_103 \def (CHead d TMP_102 u) in (let TMP_104 \def (Bind Abbr) in (let
+TMP_105 \def (CHead d0 TMP_104 u0) in (let TMP_106 \def (Bind Abbr) in (let
+TMP_107 \def (CHead d TMP_106 u) in (let TMP_108 \def (Bind Abbr) in (let
+TMP_109 \def (CHead d0 TMP_108 u0) in (let TMP_110 \def (getl_mono c TMP_107
+i H TMP_109 H15) in (let H18 \def (f_equal C T TMP_101 TMP_103 TMP_105
+TMP_110) in (let TMP_155 \def (\lambda (H19: (eq C d d0)).(let TMP_111 \def
+(\lambda (t: T).(subst0 i t x x1)) in (let H20 \def (eq_ind_r T u0 TMP_111
+H14 u H18) in (let TMP_114 \def (\lambda (t: T).(let TMP_112 \def (Bind Abbr)
+in (let TMP_113 \def (CHead d0 TMP_112 t) in (getl i c TMP_113)))) in (let
+H21 \def (eq_ind_r T u0 TMP_114 H16 u H18) in (let TMP_117 \def (\lambda (c0:
+C).(let TMP_115 \def (Bind Abbr) in (let TMP_116 \def (CHead c0 TMP_115 u) in
+(getl i c TMP_116)))) in (let H22 \def (eq_ind_r C d0 TMP_117 H21 d H19) in
+(let TMP_118 \def (eq T x1 x0) in (let TMP_119 \def (\lambda (t: T).(subst0 i
+u x1 t)) in (let TMP_120 \def (\lambda (t: T).(subst0 i u x0 t)) in (let
+TMP_121 \def (ex2 T TMP_119 TMP_120) in (let TMP_122 \def (subst0 i u x1 x0)
+in (let TMP_123 \def (subst0 i u x0 x1) in (let TMP_124 \def (\lambda (t:
+T).(pr2 c t1 t)) in (let TMP_125 \def (\lambda (t: T).(pr2 c t2 t)) in (let
+TMP_126 \def (ex2 T TMP_124 TMP_125) in (let TMP_132 \def (\lambda (H23: (eq
+T x1 x0)).(let TMP_127 \def (\lambda (t: T).(pr0 t2 t)) in (let H24 \def
+(eq_ind T x1 TMP_127 H11 x0 H23) in (let TMP_128 \def (\lambda (t: T).(pr2 c
+t1 t)) in (let TMP_129 \def (\lambda (t: T).(pr2 c t2 t)) in (let TMP_130
+\def (pr2_free c t1 x0 H8) in (let TMP_131 \def (pr2_free c t2 x0 H24) in
+(ex_intro2 T TMP_128 TMP_129 x0 TMP_130 TMP_131)))))))) in (let TMP_143 \def
+(\lambda (H23: (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t:
+T).(subst0 i u x0 t)))).(let TMP_133 \def (\lambda (t: T).(subst0 i u x1 t))
+in (let TMP_134 \def (\lambda (t: T).(subst0 i u x0 t)) in (let TMP_135 \def
+(\lambda (t: T).(pr2 c t1 t)) in (let TMP_136 \def (\lambda (t: T).(pr2 c t2
+t)) in (let TMP_137 \def (ex2 T TMP_135 TMP_136) in (let TMP_142 \def