X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr0%2Fpr0.ma;h=c95e41331b5d9a75e83fcb9ec119844ebed43714;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=57e9f7ef1594058fd4548d643ebea495e7eecbcf;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
index 57e9f7ef1..c95e41331 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
@@ -242,7 +242,7 @@ w0 x1 H6 (Bind Abbr)))) (\lambda (H11: (subst0 O x x1 x2)).(ex_intro2 T
 x2 x O H10 x1 H7))))) H8)) (pr0_subst0 t3 x0 H3 u2 w O H x H1))))) H5)) 
 (pr0_subst0 t5 x0 H4 u3 w0 O H0 x H2))))))))))))))).
 
-theorem pr0_confluence__pr0_delta_epsilon:
+theorem pr0_confluence__pr0_delta_tau:
  \forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to 
 (\forall (t4: T).((pr0 (lift (S O) O t4) t3) \to (\forall (t2: T).(ex2 T 
 (\lambda (t: T).(pr0 (THead (Bind Abbr) u2 w) t)) (\lambda (t: T).(pr0 t2 
@@ -256,7 +256,7 @@ t3 w)).(\lambda (t4: T).(\lambda (H0: (pr0 (lift (S O) O t4) t3)).(\lambda
 O) O x))).(\lambda (_: (pr0 t4 x)).(let H3 \def (eq_ind T t3 (\lambda (t: 
 T).(subst0 O u2 t w)) H (lift (S O) O x) H1) in (subst0_gen_lift_false x u2 w 
 (S O) O O (le_n O) (eq_ind_r nat (plus (S O) O) (\lambda (n: nat).(lt O n)) 
-(le_n (plus (S O) O)) (plus O (S O)) (plus_comm O (S O))) H3 (ex2 T (\lambda 
+(le_n (plus (S O) O)) (plus O (S O)) (plus_sym O (S O))) H3 (ex2 T (\lambda 
 (t: T).(pr0 (THead (Bind Abbr) u2 w) t)) (\lambda (t: T).(pr0 t2 t)))))))) 
 (pr0_gen_lift t4 t3 (S O) O H0)))))))).
 
@@ -399,22 +399,22 @@ T).(\forall (v: T).((tlt v t6) \to (\forall (t7: T).((pr0 v t7) \to (\forall
 T).(pr0 t8 t9)))))))))) H (THead (Bind b) u (lift (S O) O t4)) H7) in 
 (ex_intro2 T (\lambda (t6: T).(pr0 (THead (Bind b) u (lift (S O) O t4)) t6)) 
 (\lambda (t6: T).(pr0 t2 t6)) t2 (pr0_zeta b H10 t4 t2 H11 u) (pr0_refl 
-t2)))) t1 H12)))) t5 (sym_eq T t5 t2 H9))) t H7 H8 H5 H6))) | (pr0_epsilon t4 
-t5 H5 u) \Rightarrow (\lambda (H6: (eq T (THead (Flat Cast) u t4) 
-t)).(\lambda (H7: (eq T t5 t2)).(eq_ind T (THead (Flat Cast) u t4) (\lambda 
-(_: T).((eq T t5 t2) \to ((pr0 t4 t5) \to (ex2 T (\lambda (t7: T).(pr0 t1 
-t7)) (\lambda (t7: T).(pr0 t2 t7)))))) (\lambda (H8: (eq T t5 t2)).(eq_ind T 
-t2 (\lambda (t6: T).((pr0 t4 t6) \to (ex2 T (\lambda (t7: T).(pr0 t1 t7)) 
-(\lambda (t7: T).(pr0 t2 t7))))) (\lambda (H9: (pr0 t4 t2)).(let H10 \def 
-(eq_ind_r T t (\lambda (t6: T).(eq T t6 t1)) H4 (THead (Flat Cast) u t4) H6) 
-in (eq_ind T (THead (Flat Cast) u t4) (\lambda (t6: T).(ex2 T (\lambda (t7: 
-T).(pr0 t6 t7)) (\lambda (t7: T).(pr0 t2 t7)))) (let H11 \def (eq_ind_r T t 
-(\lambda (t6: T).(eq T t3 t6)) H2 (THead (Flat Cast) u t4) H6) in (let H12 
-\def (eq_ind_r T t (\lambda (t6: T).(\forall (v: T).((tlt v t6) \to (\forall 
-(t7: T).((pr0 v t7) \to (\forall (t8: T).((pr0 v t8) \to (ex2 T (\lambda (t9: 
+t2)))) t1 H12)))) t5 (sym_eq T t5 t2 H9))) t H7 H8 H5 H6))) | (pr0_tau t4 t5 
+H5 u) \Rightarrow (\lambda (H6: (eq T (THead (Flat Cast) u t4) t)).(\lambda 
+(H7: (eq T t5 t2)).(eq_ind T (THead (Flat Cast) u t4) (\lambda (_: T).((eq T 
+t5 t2) \to ((pr0 t4 t5) \to (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda 
+(t7: T).(pr0 t2 t7)))))) (\lambda (H8: (eq T t5 t2)).(eq_ind T t2 (\lambda 
+(t6: T).((pr0 t4 t6) \to (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: 
+T).(pr0 t2 t7))))) (\lambda (H9: (pr0 t4 t2)).(let H10 \def (eq_ind_r T t 
+(\lambda (t6: T).(eq T t6 t1)) H4 (THead (Flat Cast) u t4) H6) in (eq_ind T 
+(THead (Flat Cast) u t4) (\lambda (t6: T).(ex2 T (\lambda (t7: T).(pr0 t6 
+t7)) (\lambda (t7: T).(pr0 t2 t7)))) (let H11 \def (eq_ind_r T t (\lambda 
+(t6: T).(eq T t3 t6)) H2 (THead (Flat Cast) u t4) H6) in (let H12 \def 
+(eq_ind_r T t (\lambda (t6: T).(\forall (v: T).((tlt v t6) \to (\forall (t7: 
+T).((pr0 v t7) \to (\forall (t8: T).((pr0 v t8) \to (ex2 T (\lambda (t9: 
 T).(pr0 t7 t9)) (\lambda (t9: T).(pr0 t8 t9)))))))))) H (THead (Flat Cast) u 
 t4) H6) in (ex_intro2 T (\lambda (t6: T).(pr0 (THead (Flat Cast) u t4) t6)) 
-(\lambda (t6: T).(pr0 t2 t6)) t2 (pr0_epsilon t4 t2 H9 u) (pr0_refl t2)))) t1 
+(\lambda (t6: T).(pr0 t2 t6)) t2 (pr0_tau t4 t2 H9 u) (pr0_refl t2)))) t1 
 H10))) t5 (sym_eq T t5 t2 H8))) t H6 H7 H5)))]) in (H5 (refl_equal T t) 
 (refl_equal T t2))) t (sym_eq T t t1 H4))) t3 (sym_eq T t3 t H2) H3))) | 
 (pr0_comp u1 u2 H2 t3 t4 H3 k) \Rightarrow (\lambda (H4: (eq T (THead k u1 
@@ -646,49 +646,49 @@ t10)) (\lambda (t10: T).(pr0 (THead (Bind Abbr) v2 t6) t10)))))) (\lambda
 (t9: T).(pr0 (THead (Flat Appl) u2 t4) t9)) (\lambda (t9: T).(pr0 (THead 
 (Bind Abbr) v2 t6) t9)))) with []) in H37))) t8 (sym_eq T t8 t4 H34))) t5 
 H33)) u0 (sym_eq T u0 u H32))) b (sym_eq B b Abst H31))) H30)) H29)) H28 H25 
-H26))) | (pr0_epsilon t7 t8 H25 u0) \Rightarrow (\lambda (H26: (eq T (THead 
-(Flat Cast) u0 t7) (THead (Bind Abst) u t5))).(\lambda (H27: (eq T t8 
-t4)).((let H28 \def (eq_ind T (THead (Flat Cast) u0 t7) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in 
-K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
-\Rightarrow True])])) I (THead (Bind Abst) u t5) H26) in (False_ind ((eq T t8 
-t4) \to ((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 
-t4) t9)) (\lambda (t9: T).(pr0 (THead (Bind Abbr) v2 t6) t9))))) H28)) H27 
-H25)))]) in (H25 (refl_equal T (THead (Bind Abst) u t5)) (refl_equal T 
-t4))))) k H21))))) H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_upsilon 
-b H9 v1 v2 H10 u0 u3 H11 t5 t6 H12) \Rightarrow (\lambda (H13: (eq T (THead 
-(Flat Appl) v1 (THead (Bind b) u0 t5)) t)).(\lambda (H14: (eq T (THead (Bind 
-b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T (THead (Flat 
-Appl) v1 (THead (Bind b) u0 t5)) (\lambda (_: T).((eq T (THead (Bind b) u3 
-(THead (Flat Appl) (lift (S O) O v2) t6)) t2) \to ((not (eq B b Abst)) \to 
-((pr0 v1 v2) \to ((pr0 u0 u3) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: 
-T).(pr0 (THead k u2 t4) t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) (\lambda 
-(H15: (eq T (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) 
-t2)).(eq_ind T (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) 
-(\lambda (t7: T).((not (eq B b Abst)) \to ((pr0 v1 v2) \to ((pr0 u0 u3) \to 
-((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead k u2 t4) t8)) (\lambda 
-(t8: T).(pr0 t7 t8)))))))) (\lambda (H16: (not (eq B b Abst))).(\lambda (H17: 
-(pr0 v1 v2)).(\lambda (H18: (pr0 u0 u3)).(\lambda (H19: (pr0 t5 t6)).(let H20 
-\def (eq_ind_r T t (\lambda (t7: T).(eq T (THead k u1 t3) t7)) H4 (THead 
-(Flat Appl) v1 (THead (Bind b) u0 t5)) H13) in (let H21 \def (f_equal T K 
-(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) 
-\Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) 
+H26))) | (pr0_tau t7 t8 H25 u0) \Rightarrow (\lambda (H26: (eq T (THead (Flat 
+Cast) u0 t7) (THead (Bind Abst) u t5))).(\lambda (H27: (eq T t8 t4)).((let 
+H28 \def (eq_ind T (THead (Flat Cast) u0 t7) (\lambda (e: T).(match e in T 
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda 
+(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
+True])])) I (THead (Bind Abst) u t5) H26) in (False_ind ((eq T t8 t4) \to 
+((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t4) t9)) 
+(\lambda (t9: T).(pr0 (THead (Bind Abbr) v2 t6) t9))))) H28)) H27 H25)))]) in 
+(H25 (refl_equal T (THead (Bind Abst) u t5)) (refl_equal T t4))))) k H21))))) 
+H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_upsilon b H9 v1 v2 H10 u0 
+u3 H11 t5 t6 H12) \Rightarrow (\lambda (H13: (eq T (THead (Flat Appl) v1 
+(THead (Bind b) u0 t5)) t)).(\lambda (H14: (eq T (THead (Bind b) u3 (THead 
+(Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T (THead (Flat Appl) v1 
+(THead (Bind b) u0 t5)) (\lambda (_: T).((eq T (THead (Bind b) u3 (THead 
+(Flat Appl) (lift (S O) O v2) t6)) t2) \to ((not (eq B b Abst)) \to ((pr0 v1 
+v2) \to ((pr0 u0 u3) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead 
+k u2 t4) t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) (\lambda (H15: (eq T 
+(THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T 
+(THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) (\lambda (t7: 
+T).((not (eq B b Abst)) \to ((pr0 v1 v2) \to ((pr0 u0 u3) \to ((pr0 t5 t6) 
+\to (ex2 T (\lambda (t8: T).(pr0 (THead k u2 t4) t8)) (\lambda (t8: T).(pr0 
+t7 t8)))))))) (\lambda (H16: (not (eq B b Abst))).(\lambda (H17: (pr0 v1 
+v2)).(\lambda (H18: (pr0 u0 u3)).(\lambda (H19: (pr0 t5 t6)).(let H20 \def 
+(eq_ind_r T t (\lambda (t7: T).(eq T (THead k u1 t3) t7)) H4 (THead (Flat 
+Appl) v1 (THead (Bind b) u0 t5)) H13) in (let H21 \def (f_equal T K (\lambda 
+(e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k 
+| (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
+(THead (Flat Appl) v1 (THead (Bind b) u0 t5)) H20) in ((let H22 \def (f_equal 
+T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t7 _) \Rightarrow t7])) 
 (THead k u1 t3) (THead (Flat Appl) v1 (THead (Bind b) u0 t5)) H20) in ((let 
-H22 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
-with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t7 _) 
+H23 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
+with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t7) 
 \Rightarrow t7])) (THead k u1 t3) (THead (Flat Appl) v1 (THead (Bind b) u0 
-t5)) H20) in ((let H23 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 
-| (THead _ _ t7) \Rightarrow t7])) (THead k u1 t3) (THead (Flat Appl) v1 
-(THead (Bind b) u0 t5)) H20) in (\lambda (H24: (eq T u1 v1)).(\lambda (H25: 
-(eq K k (Flat Appl))).(let H26 \def (eq_ind_r T t (\lambda (t7: T).(\forall 
-(v: T).((tlt v t7) \to (\forall (t8: T).((pr0 v t8) \to (\forall (t9: 
-T).((pr0 v t9) \to (ex2 T (\lambda (t10: T).(pr0 t8 t10)) (\lambda (t10: 
-T).(pr0 t9 t10)))))))))) H (THead (Flat Appl) v1 (THead (Bind b) u0 t5)) H13) 
-in (eq_ind_r K (Flat Appl) (\lambda (k0: K).(ex2 T (\lambda (t7: T).(pr0 
-(THead k0 u2 t4) t7)) (\lambda (t7: T).(pr0 (THead (Bind b) u3 (THead (Flat 
-Appl) (lift (S O) O v2) t6)) t7)))) (let H27 \def (eq_ind T u1 (\lambda (t7: 
+t5)) H20) in (\lambda (H24: (eq T u1 v1)).(\lambda (H25: (eq K k (Flat 
+Appl))).(let H26 \def (eq_ind_r T t (\lambda (t7: T).(\forall (v: T).((tlt v 
+t7) \to (\forall (t8: T).((pr0 v t8) \to (\forall (t9: T).((pr0 v t9) \to 
+(ex2 T (\lambda (t10: T).(pr0 t8 t10)) (\lambda (t10: T).(pr0 t9 
+t10)))))))))) H (THead (Flat Appl) v1 (THead (Bind b) u0 t5)) H13) in 
+(eq_ind_r K (Flat Appl) (\lambda (k0: K).(ex2 T (\lambda (t7: T).(pr0 (THead 
+k0 u2 t4) t7)) (\lambda (t7: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) 
+(lift (S O) O v2) t6)) t7)))) (let H27 \def (eq_ind T u1 (\lambda (t7: 
 T).(pr0 t7 u2)) H7 v1 H24) in (let H28 \def (eq_ind T t3 (\lambda (t7: 
 T).(pr0 t7 t4)) H8 (THead (Bind b) u0 t5) H23) in (let H29 \def (match H28 in 
 pr0 return (\lambda (t7: T).(\lambda (t8: T).(\lambda (_: (pr0 t7 t8)).((eq T 
@@ -911,8 +911,8 @@ O t7))) (lift_tlt_dx (Bind b) u0 t7 (S O) O) (tlt_head_dx (Flat Appl) v1
 (THead (Bind b) u0 (lift (S O) O t7)))) x H45 t4 H40)) t6 H44)))) 
 (pr0_gen_lift t7 t6 (S O) O H43))))))) t8 (sym_eq T t8 t4 H38))) t5 H37)) u 
 (sym_eq T u u0 H36))) b0 (sym_eq B b0 b H35))) H34)) H33)) H32 H29 H30))) | 
-(pr0_epsilon t7 t8 H29 u) \Rightarrow (\lambda (H30: (eq T (THead (Flat Cast) 
-u t7) (THead (Bind b) u0 t5))).(\lambda (H31: (eq T t8 t4)).((let H32 \def 
+(pr0_tau t7 t8 H29 u) \Rightarrow (\lambda (H30: (eq T (THead (Flat Cast) u 
+t7) (THead (Bind b) u0 t5))).(\lambda (H31: (eq T t8 t4)).((let H32 \def 
 (eq_ind T (THead (Flat Cast) u t7) (\lambda (e: T).(match e in T return 
 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
 \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda 
@@ -1000,10 +1000,10 @@ x x0)).(\lambda (H28: (pr0 t2 x0)).(ex_intro2 T (\lambda (t7: T).(pr0 (THead
 (Bind b) u2 (lift (S O) O x)) t7)) (\lambda (t7: T).(pr0 t2 t7)) x0 (pr0_zeta 
 b H14 x x0 H27 u2) H28)))) (H22 t5 (lift_tlt_dx (Bind b) u t5 (S O) O) x H26 
 t2 H15)) t4 H25)))) (pr0_gen_lift t5 t4 (S O) O H24)))) k H21))))) H18)) 
-H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | (pr0_epsilon t5 t6 
-H9 u) \Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u t5) t)).(\lambda 
-(H11: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u t5) (\lambda (_: T).((eq T 
-t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead k u2 t4) t8)) 
+H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | (pr0_tau t5 t6 H9 u) 
+\Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u t5) t)).(\lambda (H11: 
+(eq T t6 t2)).(eq_ind T (THead (Flat Cast) u t5) (\lambda (_: T).((eq T t6 
+t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead k u2 t4) t8)) 
 (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H12: (eq T t6 t2)).(eq_ind T t2 
 (\lambda (t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8: T).(pr0 (THead k u2 
 t4) t8)) (\lambda (t8: T).(pr0 t2 t8))))) (\lambda (H13: (pr0 t5 t2)).(let 
@@ -1029,9 +1029,9 @@ t5 H17) in (ex2_ind T (\lambda (t7: T).(pr0 t4 t7)) (\lambda (t7: T).(pr0 t2
 t7)) (ex2 T (\lambda (t7: T).(pr0 (THead (Flat Cast) u2 t4) t7)) (\lambda 
 (t7: T).(pr0 t2 t7))) (\lambda (x: T).(\lambda (H23: (pr0 t4 x)).(\lambda 
 (H24: (pr0 t2 x)).(ex_intro2 T (\lambda (t7: T).(pr0 (THead (Flat Cast) u2 
-t4) t7)) (\lambda (t7: T).(pr0 t2 t7)) x (pr0_epsilon t4 x H23 u2) H24)))) 
-(H20 t5 (tlt_head_dx (Flat Cast) u t5) t4 H22 t2 H13)))) k H19))))) H16)) 
-H15)))) t6 (sym_eq T t6 t2 H12))) t H10 H11 H9)))]) in (H9 (refl_equal T t) 
+t4) t7)) (\lambda (t7: T).(pr0 t2 t7)) x (pr0_tau t4 x H23 u2) H24)))) (H20 
+t5 (tlt_head_dx (Flat Cast) u t5) t4 H22 t2 H13)))) k H19))))) H16)) H15)))) 
+t6 (sym_eq T t6 t2 H12))) t H10 H11 H9)))]) in (H9 (refl_equal T t) 
 (refl_equal T t2))))) t1 H6)) t H4 H5 H2 H3))) | (pr0_beta u v1 v2 H2 t3 t4 
 H3) \Rightarrow (\lambda (H4: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) 
 u t3)) t)).(\lambda (H5: (eq T (THead (Bind Abbr) v2 t4) t1)).(eq_ind T 
@@ -1239,76 +1239,76 @@ t10)) (\lambda (t10: T).(pr0 (THead (Flat Appl) u2 t6) t10)))))) (\lambda
 (t9: T).(pr0 (THead (Bind Abbr) v2 t4) t9)) (\lambda (t9: T).(pr0 (THead 
 (Flat Appl) u2 t6) t9)))) with []) in H36))) t8 (sym_eq T t8 t6 H33))) t3 
 H32)) u0 (sym_eq T u0 u H31))) b (sym_eq B b Abst H30))) H29)) H28)) H27 H24 
-H25))) | (pr0_epsilon t7 t8 H24 u0) \Rightarrow (\lambda (H25: (eq T (THead 
-(Flat Cast) u0 t7) (THead (Bind Abst) u t3))).(\lambda (H26: (eq T t8 
-t6)).((let H27 \def (eq_ind T (THead (Flat Cast) u0 t7) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in 
-K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
-\Rightarrow True])])) I (THead (Bind Abst) u t3) H25) in (False_ind ((eq T t8 
-t6) \to ((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Bind Abbr) v2 
-t4) t9)) (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t6) t9))))) H27)) H26 
-H24)))]) in (H24 (refl_equal T (THead (Bind Abst) u t3)) (refl_equal T 
-t6))))) k H21)))) H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_beta u0 
-v0 v3 H9 t5 t6 H10) \Rightarrow (\lambda (H11: (eq T (THead (Flat Appl) v0 
-(THead (Bind Abst) u0 t5)) t)).(\lambda (H12: (eq T (THead (Bind Abbr) v3 t6) 
-t2)).(eq_ind T (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) (\lambda (_: 
-T).((eq T (THead (Bind Abbr) v3 t6) t2) \to ((pr0 v0 v3) \to ((pr0 t5 t6) \to 
+H25))) | (pr0_tau t7 t8 H24 u0) \Rightarrow (\lambda (H25: (eq T (THead (Flat 
+Cast) u0 t7) (THead (Bind Abst) u t3))).(\lambda (H26: (eq T t8 t6)).((let 
+H27 \def (eq_ind T (THead (Flat Cast) u0 t7) (\lambda (e: T).(match e in T 
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda 
+(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
+True])])) I (THead (Bind Abst) u t3) H25) in (False_ind ((eq T t8 t6) \to 
+((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Bind Abbr) v2 t4) t9)) 
+(\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t6) t9))))) H27)) H26 H24)))]) in 
+(H24 (refl_equal T (THead (Bind Abst) u t3)) (refl_equal T t6))))) k H21)))) 
+H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_beta u0 v0 v3 H9 t5 t6 
+H10) \Rightarrow (\lambda (H11: (eq T (THead (Flat Appl) v0 (THead (Bind 
+Abst) u0 t5)) t)).(\lambda (H12: (eq T (THead (Bind Abbr) v3 t6) t2)).(eq_ind 
+T (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) (\lambda (_: T).((eq T 
+(THead (Bind Abbr) v3 t6) t2) \to ((pr0 v0 v3) \to ((pr0 t5 t6) \to (ex2 T 
+(\lambda (t8: T).(pr0 (THead (Bind Abbr) v2 t4) t8)) (\lambda (t8: T).(pr0 t2 
+t8))))))) (\lambda (H13: (eq T (THead (Bind Abbr) v3 t6) t2)).(eq_ind T 
+(THead (Bind Abbr) v3 t6) (\lambda (t7: T).((pr0 v0 v3) \to ((pr0 t5 t6) \to 
 (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) v2 t4) t8)) (\lambda (t8: 
-T).(pr0 t2 t8))))))) (\lambda (H13: (eq T (THead (Bind Abbr) v3 t6) 
-t2)).(eq_ind T (THead (Bind Abbr) v3 t6) (\lambda (t7: T).((pr0 v0 v3) \to 
+T).(pr0 t7 t8)))))) (\lambda (H14: (pr0 v0 v3)).(\lambda (H15: (pr0 t5 
+t6)).(let H16 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Appl) v1 
+(THead (Bind Abst) u t3)) t7)) H4 (THead (Flat Appl) v0 (THead (Bind Abst) u0 
+t5)) H11) in (let H17 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 
+| (THead _ t7 _) \Rightarrow t7])) (THead (Flat Appl) v1 (THead (Bind Abst) u 
+t3)) (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) H16) in ((let H18 \def 
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
+[(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ _ t7) 
+\Rightarrow (match t7 in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t8 _) \Rightarrow t8])])) 
+(THead (Flat Appl) v1 (THead (Bind Abst) u t3)) (THead (Flat Appl) v0 (THead 
+(Bind Abst) u0 t5)) H16) in ((let H19 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | 
+(TLRef _) \Rightarrow t3 | (THead _ _ t7) \Rightarrow (match t7 in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 
+| (THead _ _ t8) \Rightarrow t8])])) (THead (Flat Appl) v1 (THead (Bind Abst) 
+u t3)) (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) H16) in (\lambda (_: 
+(eq T u u0)).(\lambda (H21: (eq T v1 v0)).(let H22 \def (eq_ind_r T t 
+(\lambda (t7: T).(\forall (v: T).((tlt v t7) \to (\forall (t8: T).((pr0 v t8) 
+\to (\forall (t9: T).((pr0 v t9) \to (ex2 T (\lambda (t10: T).(pr0 t8 t10)) 
+(\lambda (t10: T).(pr0 t9 t10)))))))))) H (THead (Flat Appl) v0 (THead (Bind 
+Abst) u0 t5)) H11) in (let H23 \def (eq_ind T v1 (\lambda (t7: T).(pr0 t7 
+v2)) H7 v0 H21) in (let H24 \def (eq_ind T t3 (\lambda (t7: T).(pr0 t7 t4)) 
+H8 t5 H19) in (ex2_ind T (\lambda (t7: T).(pr0 t4 t7)) (\lambda (t7: T).(pr0 
+t6 t7)) (ex2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) v2 t4) t7)) (\lambda 
+(t7: T).(pr0 (THead (Bind Abbr) v3 t6) t7))) (\lambda (x: T).(\lambda (H25: 
+(pr0 t4 x)).(\lambda (H26: (pr0 t6 x)).(ex2_ind T (\lambda (t7: T).(pr0 v2 
+t7)) (\lambda (t7: T).(pr0 v3 t7)) (ex2 T (\lambda (t7: T).(pr0 (THead (Bind 
+Abbr) v2 t4) t7)) (\lambda (t7: T).(pr0 (THead (Bind Abbr) v3 t6) t7))) 
+(\lambda (x0: T).(\lambda (H27: (pr0 v2 x0)).(\lambda (H28: (pr0 v3 
+x0)).(ex_intro2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) v2 t4) t7)) 
+(\lambda (t7: T).(pr0 (THead (Bind Abbr) v3 t6) t7)) (THead (Bind Abbr) x0 x) 
+(pr0_comp v2 x0 H27 t4 x H25 (Bind Abbr)) (pr0_comp v3 x0 H28 t6 x H26 (Bind 
+Abbr)))))) (H22 v0 (tlt_head_sx (Flat Appl) v0 (THead (Bind Abst) u0 t5)) v2 
+H23 v3 H14))))) (H22 t5 (tlt_trans (THead (Bind Abst) u0 t5) t5 (THead (Flat 
+Appl) v0 (THead (Bind Abst) u0 t5)) (tlt_head_dx (Bind Abst) u0 t5) 
+(tlt_head_dx (Flat Appl) v0 (THead (Bind Abst) u0 t5))) t4 H24 t6 H15)))))))) 
+H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_upsilon b H9 v0 v3 H10 u1 
+u2 H11 t5 t6 H12) \Rightarrow (\lambda (H13: (eq T (THead (Flat Appl) v0 
+(THead (Bind b) u1 t5)) t)).(\lambda (H14: (eq T (THead (Bind b) u2 (THead 
+(Flat Appl) (lift (S O) O v3) t6)) t2)).(eq_ind T (THead (Flat Appl) v0 
+(THead (Bind b) u1 t5)) (\lambda (_: T).((eq T (THead (Bind b) u2 (THead 
+(Flat Appl) (lift (S O) O v3) t6)) t2) \to ((not (eq B b Abst)) \to ((pr0 v0 
+v3) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead 
+(Bind Abbr) v2 t4) t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) (\lambda (H15: 
+(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v3) t6)) 
+t2)).(eq_ind T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v3) t6)) 
+(\lambda (t7: T).((not (eq B b Abst)) \to ((pr0 v0 v3) \to ((pr0 u1 u2) \to 
 ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) v2 t4) t8)) 
-(\lambda (t8: T).(pr0 t7 t8)))))) (\lambda (H14: (pr0 v0 v3)).(\lambda (H15: 
-(pr0 t5 t6)).(let H16 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat 
-Appl) v1 (THead (Bind Abst) u t3)) t7)) H4 (THead (Flat Appl) v0 (THead (Bind 
-Abst) u0 t5)) H11) in (let H17 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) 
-\Rightarrow v1 | (THead _ t7 _) \Rightarrow t7])) (THead (Flat Appl) v1 
-(THead (Bind Abst) u t3)) (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) 
-H16) in ((let H18 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | 
-(THead _ _ t7) \Rightarrow (match t7 in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t8 _) 
-\Rightarrow t8])])) (THead (Flat Appl) v1 (THead (Bind Abst) u t3)) (THead 
-(Flat Appl) v0 (THead (Bind Abst) u0 t5)) H16) in ((let H19 \def (f_equal T T 
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t7) \Rightarrow (match 
-t7 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) 
-\Rightarrow t3 | (THead _ _ t8) \Rightarrow t8])])) (THead (Flat Appl) v1 
-(THead (Bind Abst) u t3)) (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) 
-H16) in (\lambda (_: (eq T u u0)).(\lambda (H21: (eq T v1 v0)).(let H22 \def 
-(eq_ind_r T t (\lambda (t7: T).(\forall (v: T).((tlt v t7) \to (\forall (t8: 
-T).((pr0 v t8) \to (\forall (t9: T).((pr0 v t9) \to (ex2 T (\lambda (t10: 
-T).(pr0 t8 t10)) (\lambda (t10: T).(pr0 t9 t10)))))))))) H (THead (Flat Appl) 
-v0 (THead (Bind Abst) u0 t5)) H11) in (let H23 \def (eq_ind T v1 (\lambda 
-(t7: T).(pr0 t7 v2)) H7 v0 H21) in (let H24 \def (eq_ind T t3 (\lambda (t7: 
-T).(pr0 t7 t4)) H8 t5 H19) in (ex2_ind T (\lambda (t7: T).(pr0 t4 t7)) 
-(\lambda (t7: T).(pr0 t6 t7)) (ex2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) 
-v2 t4) t7)) (\lambda (t7: T).(pr0 (THead (Bind Abbr) v3 t6) t7))) (\lambda 
-(x: T).(\lambda (H25: (pr0 t4 x)).(\lambda (H26: (pr0 t6 x)).(ex2_ind T 
-(\lambda (t7: T).(pr0 v2 t7)) (\lambda (t7: T).(pr0 v3 t7)) (ex2 T (\lambda 
-(t7: T).(pr0 (THead (Bind Abbr) v2 t4) t7)) (\lambda (t7: T).(pr0 (THead 
-(Bind Abbr) v3 t6) t7))) (\lambda (x0: T).(\lambda (H27: (pr0 v2 
-x0)).(\lambda (H28: (pr0 v3 x0)).(ex_intro2 T (\lambda (t7: T).(pr0 (THead 
-(Bind Abbr) v2 t4) t7)) (\lambda (t7: T).(pr0 (THead (Bind Abbr) v3 t6) t7)) 
-(THead (Bind Abbr) x0 x) (pr0_comp v2 x0 H27 t4 x H25 (Bind Abbr)) (pr0_comp 
-v3 x0 H28 t6 x H26 (Bind Abbr)))))) (H22 v0 (tlt_head_sx (Flat Appl) v0 
-(THead (Bind Abst) u0 t5)) v2 H23 v3 H14))))) (H22 t5 (tlt_trans (THead (Bind 
-Abst) u0 t5) t5 (THead (Flat Appl) v0 (THead (Bind Abst) u0 t5)) (tlt_head_dx 
-(Bind Abst) u0 t5) (tlt_head_dx (Flat Appl) v0 (THead (Bind Abst) u0 t5))) t4 
-H24 t6 H15)))))))) H18)) H17))))) t2 H13)) t H11 H12 H9 H10))) | (pr0_upsilon 
-b H9 v0 v3 H10 u1 u2 H11 t5 t6 H12) \Rightarrow (\lambda (H13: (eq T (THead 
-(Flat Appl) v0 (THead (Bind b) u1 t5)) t)).(\lambda (H14: (eq T (THead (Bind 
-b) u2 (THead (Flat Appl) (lift (S O) O v3) t6)) t2)).(eq_ind T (THead (Flat 
-Appl) v0 (THead (Bind b) u1 t5)) (\lambda (_: T).((eq T (THead (Bind b) u2 
-(THead (Flat Appl) (lift (S O) O v3) t6)) t2) \to ((not (eq B b Abst)) \to 
-((pr0 v0 v3) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: 
-T).(pr0 (THead (Bind Abbr) v2 t4) t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) 
-(\lambda (H15: (eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v3) 
-t6)) t2)).(eq_ind T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v3) 
-t6)) (\lambda (t7: T).((not (eq B b Abst)) \to ((pr0 v0 v3) \to ((pr0 u1 u2) 
-\to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) v2 t4) 
-t8)) (\lambda (t8: T).(pr0 t7 t8)))))))) (\lambda (H16: (not (eq B b 
+(\lambda (t8: T).(pr0 t7 t8)))))))) (\lambda (H16: (not (eq B b 
 Abst))).(\lambda (_: (pr0 v0 v3)).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (pr0 
 t5 t6)).(let H20 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Appl) 
 v1 (THead (Bind Abst) u t3)) t7)) H4 (THead (Flat Appl) v0 (THead (Bind b) u1 
@@ -1378,8 +1378,8 @@ T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
 True])])) I (THead (Bind b) u0 (lift (S O) O t5)) H16) in (False_ind (ex2 T 
 (\lambda (t7: T).(pr0 (THead (Bind Abbr) v2 t4) t7)) (\lambda (t7: T).(pr0 t2 
-t7))) H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | (pr0_epsilon 
-t5 t6 H9 u0) \Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u0 t5) 
+t7))) H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | (pr0_tau t5 t6 
+H9 u0) \Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u0 t5) 
 t)).(\lambda (H11: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u0 t5) (\lambda 
 (_: T).((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead 
 (Bind Abbr) v2 t4) t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H12: (eq 
@@ -1706,12 +1706,12 @@ b) u1 (lift (S O) O t7))) (lift_tlt_dx (Bind b) u1 t7 (S O) O) (tlt_head_dx
 u0 (tlt_head_sx (Flat Appl) u0 (THead (Bind b) u1 (lift (S O) O t7))) v2 H46 
 u3 H18))) t4 H44)))) (pr0_gen_lift t7 t4 (S O) O H43)))))))) t8 (sym_eq T t8 
 t6 H37))) t3 H36)) u (sym_eq T u u1 H35))) b0 (sym_eq B b0 b H34))) H33)) 
-H32)) H31 H28 H29))) | (pr0_epsilon t7 t8 H28 u) \Rightarrow (\lambda (H29: 
-(eq T (THead (Flat Cast) u t7) (THead (Bind b) u1 t3))).(\lambda (H30: (eq T 
-t8 t6)).((let H31 \def (eq_ind T (THead (Flat Cast) u t7) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in 
-K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
+H32)) H31 H28 H29))) | (pr0_tau t7 t8 H28 u) \Rightarrow (\lambda (H29: (eq T 
+(THead (Flat Cast) u t7) (THead (Bind b) u1 t3))).(\lambda (H30: (eq T t8 
+t6)).((let H31 \def (eq_ind T (THead (Flat Cast) u t7) (\lambda (e: T).(match 
+e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
+(TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K 
+return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
 \Rightarrow True])])) I (THead (Bind b) u1 t3) H29) in (False_ind ((eq T t8 
 t6) \to ((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Bind b) u2 
 (THead (Flat Appl) (lift (S O) O v2) t4)) t9)) (\lambda (t9: T).(pr0 (THead 
@@ -1874,7 +1874,7 @@ t2)).(let H20 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Appl) v1
 (Flat _) \Rightarrow True])])) I (THead (Bind b0) u (lift (S O) O t5)) H20) 
 in (False_ind (ex2 T (\lambda (t7: T).(pr0 (THead (Bind b) u2 (THead (Flat 
 Appl) (lift (S O) O v2) t4)) t7)) (\lambda (t7: T).(pr0 t2 t7))) H21))))) t6 
-(sym_eq T t6 t2 H17))) t H15 H16 H13 H14))) | (pr0_epsilon t5 t6 H13 u) 
+(sym_eq T t6 t2 H17))) t H15 H16 H13 H14))) | (pr0_tau t5 t6 H13 u) 
 \Rightarrow (\lambda (H14: (eq T (THead (Flat Cast) u t5) t)).(\lambda (H15: 
 (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u t5) (\lambda (_: T).((eq T t6 
 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind b) u2 
@@ -2075,10 +2075,10 @@ T).(subst0 O u2 t7 w)) H10 (lift (S O) O x) H29) in (ex2_ind T (\lambda (t7:
 T).(pr0 x t7)) (\lambda (t7: T).(pr0 t2 t7)) (ex2 T (\lambda (t7: T).(pr0 
 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 t2 t7))) (\lambda (x0: 
 T).(\lambda (_: (pr0 x x0)).(\lambda (_: (pr0 t2 
-x0)).(pr0_confluence__pr0_delta_epsilon u2 (lift (S O) O x) w H31 x (pr0_refl 
+x0)).(pr0_confluence__pr0_delta_tau u2 (lift (S O) O x) w H31 x (pr0_refl 
 (lift (S O) O x)) t2)))) (H26 t5 (lift_tlt_dx (Bind Abbr) u t5 (S O) O) x H30 
 t2 H17)))))) (pr0_gen_lift t5 t4 (S O) O H28)))))))))) H20)) H19))))) t6 
-(sym_eq T t6 t2 H15))) t H13 H14 H11 H12))) | (pr0_epsilon t5 t6 H11 u) 
+(sym_eq T t6 t2 H15))) t H13 H14 H11 H12))) | (pr0_tau t5 t6 H11 u) 
 \Rightarrow (\lambda (H12: (eq T (THead (Flat Cast) u t5) t)).(\lambda (H13: 
 (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u t5) (\lambda (_: T).((eq T t6 
 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) u2 
@@ -2259,156 +2259,155 @@ T).(pr0 t3 t7)) (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0
 (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead (Bind Abbr) u2 w) 
 t7))) (\lambda (x0: T).(\lambda (_: (pr0 x x0)).(\lambda (_: (pr0 t1 
 x0)).(ex2_sym T (pr0 (THead (Bind Abbr) u2 w)) (pr0 t1) 
-(pr0_confluence__pr0_delta_epsilon u2 (lift (S O) O x) w H29 x (pr0_refl 
-(lift (S O) O x)) t1))))) (H28 t3 (lift_tlt_dx (Bind Abbr) u1 t3 (S O) O) x 
-H26 t1 H8))))))))) (pr0_gen_lift t3 t6 (S O) O H24)))))) H20)) H19)))))) t2 
-H14)) t H12 H13 H9 H10 H11))) | (pr0_zeta b0 H9 t5 t6 H10 u0) \Rightarrow 
-(\lambda (H11: (eq T (THead (Bind b0) u0 (lift (S O) O t5)) t)).(\lambda 
-(H12: (eq T t6 t2)).(eq_ind T (THead (Bind b0) u0 (lift (S O) O t5)) (\lambda 
-(_: T).((eq T t6 t2) \to ((not (eq B b0 Abst)) \to ((pr0 t5 t6) \to (ex2 T 
-(\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))) (\lambda 
-(H13: (eq T t6 t2)).(eq_ind T t2 (\lambda (t7: T).((not (eq B b0 Abst)) \to 
-((pr0 t5 t7) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 
-t2 t8)))))) (\lambda (_: (not (eq B b0 Abst))).(\lambda (H15: (pr0 t5 
-t2)).(let H16 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Bind b) u 
-(lift (S O) O t3)) t7)) H4 (THead (Bind b0) u0 (lift (S O) O t5)) H11) in 
-(let H17 \def (f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: 
-T).B) with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1) 
-\Rightarrow b1 | (Flat _) \Rightarrow b])])) (THead (Bind b) u (lift (S O) O 
-t3)) (THead (Bind b0) u0 (lift (S O) O t5)) H16) in ((let H18 \def (f_equal T 
-T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t7 _) \Rightarrow t7])) 
-(THead (Bind b) u (lift (S O) O t3)) (THead (Bind b0) u0 (lift (S O) O t5)) 
-H16) in ((let H19 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map (f: ((nat 
-\to nat))) (d: nat) (t7: T) on t7: T \def (match t7 with [(TSort n) 
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with 
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u1 t8) 
-\Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) t8))]) in 
-lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _) \Rightarrow 
-((let rec lref_map (f: ((nat \to nat))) (d: nat) (t7: T) on t7: T \def (match 
-t7 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef 
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | 
-(THead k u1 t8) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) 
-t8))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _ t7) 
-\Rightarrow t7])) (THead (Bind b) u (lift (S O) O t3)) (THead (Bind b0) u0 
-(lift (S O) O t5)) H16) in (\lambda (_: (eq T u u0)).(\lambda (H21: (eq B b 
-b0)).(let H22 \def (eq_ind_r T t (\lambda (t7: T).(\forall (v: T).((tlt v t7) 
-\to (\forall (t8: T).((pr0 v t8) \to (\forall (t9: T).((pr0 v t9) \to (ex2 T 
-(\lambda (t10: T).(pr0 t8 t10)) (\lambda (t10: T).(pr0 t9 t10)))))))))) H 
-(THead (Bind b0) u0 (lift (S O) O t5)) H11) in (let H23 \def (eq_ind T t3 
-(\lambda (t7: T).(pr0 t7 t1)) H8 t5 (lift_inj t3 t5 (S O) O H19)) in (let H24 
-\def (eq_ind B b (\lambda (b1: B).(not (eq B b1 Abst))) H7 b0 H21) in 
-(ex2_ind T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)) (ex2 T 
-(\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7))) (\lambda (x: 
-T).(\lambda (H25: (pr0 t1 x)).(\lambda (H26: (pr0 t2 x)).(ex_intro2 T 
-(\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)) x H25 H26)))) 
-(H22 t5 (lift_tlt_dx (Bind b0) u0 t5 (S O) O) t1 H23 t2 H15)))))))) H18)) 
-H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | (pr0_epsilon t5 t6 
-H9 u0) \Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u0 t5) 
-t)).(\lambda (H11: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u0 t5) (\lambda 
-(_: T).((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 
-t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H12: (eq T t6 t2)).(eq_ind T 
-t2 (\lambda (t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) 
-(\lambda (t8: T).(pr0 t2 t8))))) (\lambda (_: (pr0 t5 t2)).(let H14 \def 
+(pr0_confluence__pr0_delta_tau u2 (lift (S O) O x) w H29 x (pr0_refl (lift (S 
+O) O x)) t1))))) (H28 t3 (lift_tlt_dx (Bind Abbr) u1 t3 (S O) O) x H26 t1 
+H8))))))))) (pr0_gen_lift t3 t6 (S O) O H24)))))) H20)) H19)))))) t2 H14)) t 
+H12 H13 H9 H10 H11))) | (pr0_zeta b0 H9 t5 t6 H10 u0) \Rightarrow (\lambda 
+(H11: (eq T (THead (Bind b0) u0 (lift (S O) O t5)) t)).(\lambda (H12: (eq T 
+t6 t2)).(eq_ind T (THead (Bind b0) u0 (lift (S O) O t5)) (\lambda (_: T).((eq 
+T t6 t2) \to ((not (eq B b0 Abst)) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: 
+T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))) (\lambda (H13: (eq T t6 
+t2)).(eq_ind T t2 (\lambda (t7: T).((not (eq B b0 Abst)) \to ((pr0 t5 t7) \to 
+(ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8)))))) 
+(\lambda (_: (not (eq B b0 Abst))).(\lambda (H15: (pr0 t5 t2)).(let H16 \def 
 (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Bind b) u (lift (S O) O t3)) 
-t7)) H4 (THead (Flat Cast) u0 t5) H10) in (let H15 \def (eq_ind T (THead 
-(Bind b) u (lift (S O) O t3)) (\lambda (ee: T).(match ee in T return (\lambda 
-(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
-| (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
-Cast) u0 t5) H14) in (False_ind (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda 
-(t7: T).(pr0 t2 t7))) H15)))) t6 (sym_eq T t6 t2 H12))) t H10 H11 H9)))]) in 
-(H9 (refl_equal T t) (refl_equal T t2))))) t4 (sym_eq T t4 t1 H6))) t H4 H5 
-H2 H3))) | (pr0_epsilon t3 t4 H2 u) \Rightarrow (\lambda (H3: (eq T (THead 
-(Flat Cast) u t3) t)).(\lambda (H4: (eq T t4 t1)).(eq_ind T (THead (Flat 
-Cast) u t3) (\lambda (_: T).((eq T t4 t1) \to ((pr0 t3 t4) \to (ex2 T 
-(\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 t2 t6)))))) (\lambda (H5: 
-(eq T t4 t1)).(eq_ind T t1 (\lambda (t5: T).((pr0 t3 t5) \to (ex2 T (\lambda 
-(t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 t2 t6))))) (\lambda (H6: (pr0 t3 
-t1)).(let H7 \def (match H1 in pr0 return (\lambda (t5: T).(\lambda (t6: 
-T).(\lambda (_: (pr0 t5 t6)).((eq T t5 t) \to ((eq T t6 t2) \to (ex2 T 
-(\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)))))))) with 
-[(pr0_refl t5) \Rightarrow (\lambda (H7: (eq T t5 t)).(\lambda (H8: (eq T t5 
-t2)).(eq_ind T t (\lambda (t6: T).((eq T t6 t2) \to (ex2 T (\lambda (t7: 
-T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7))))) (\lambda (H9: (eq T t 
-t2)).(eq_ind T t2 (\lambda (_: T).(ex2 T (\lambda (t7: T).(pr0 t1 t7)) 
-(\lambda (t7: T).(pr0 t2 t7)))) (let H10 \def (eq_ind_r T t (\lambda (t6: 
-T).(eq T t6 t2)) H9 (THead (Flat Cast) u t3) H3) in (eq_ind T (THead (Flat 
-Cast) u t3) (\lambda (t6: T).(ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda 
-(t7: T).(pr0 t6 t7)))) (let H11 \def (eq_ind_r T t (\lambda (t6: T).(eq T t5 
-t6)) H7 (THead (Flat Cast) u t3) H3) in (let H12 \def (eq_ind_r T t (\lambda 
-(t6: T).(\forall (v: T).((tlt v t6) \to (\forall (t7: T).((pr0 v t7) \to 
-(\forall (t8: T).((pr0 v t8) \to (ex2 T (\lambda (t9: T).(pr0 t7 t9)) 
-(\lambda (t9: T).(pr0 t8 t9)))))))))) H (THead (Flat Cast) u t3) H3) in 
-(ex_intro2 T (\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 (THead (Flat 
-Cast) u t3) t6)) t1 (pr0_refl t1) (pr0_epsilon t3 t1 H6 u)))) t2 H10)) t 
-(sym_eq T t t2 H9))) t5 (sym_eq T t5 t H7) H8))) | (pr0_comp u1 u2 H7 t5 t6 
-H8 k) \Rightarrow (\lambda (H9: (eq T (THead k u1 t5) t)).(\lambda (H10: (eq 
-T (THead k u2 t6) t2)).(eq_ind T (THead k u1 t5) (\lambda (_: T).((eq T 
-(THead k u2 t6) t2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda 
-(t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))) (\lambda (H11: (eq T 
-(THead k u2 t6) t2)).(eq_ind T (THead k u2 t6) (\lambda (t7: T).((pr0 u1 u2) 
-\to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: 
-T).(pr0 t7 t8)))))) (\lambda (_: (pr0 u1 u2)).(\lambda (H13: (pr0 t5 
-t6)).(let H14 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Cast) u 
-t3) t7)) H3 (THead k u1 t5) H9) in (let H15 \def (f_equal T K (\lambda (e: 
-T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow (Flat 
-Cast) | (TLRef _) \Rightarrow (Flat Cast) | (THead k0 _ _) \Rightarrow k0])) 
-(THead (Flat Cast) u t3) (THead k u1 t5) H14) in ((let H16 \def (f_equal T T 
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t7 _) \Rightarrow t7])) 
-(THead (Flat Cast) u t3) (THead k u1 t5) H14) in ((let H17 \def (f_equal T T 
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t7) \Rightarrow t7])) 
-(THead (Flat Cast) u t3) (THead k u1 t5) H14) in (\lambda (_: (eq T u 
-u1)).(\lambda (H19: (eq K (Flat Cast) k)).(eq_ind K (Flat Cast) (\lambda (k0: 
-K).(ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead k0 u2 
-t6) t7)))) (let H20 \def (eq_ind_r K k (\lambda (k0: K).(eq T (THead k0 u1 
-t5) t)) H9 (Flat Cast) H19) in (let H21 \def (eq_ind_r T t (\lambda (t7: 
+t7)) H4 (THead (Bind b0) u0 (lift (S O) O t5)) H11) in (let H17 \def (f_equal 
+T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with [(TSort _) 
+\Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _) \Rightarrow (match k 
+in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) 
+\Rightarrow b])])) (THead (Bind b) u (lift (S O) O t3)) (THead (Bind b0) u0 
+(lift (S O) O t5)) H16) in ((let H18 \def (f_equal T T (\lambda (e: T).(match 
+e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) 
+\Rightarrow u | (THead _ t7 _) \Rightarrow t7])) (THead (Bind b) u (lift (S 
+O) O t3)) (THead (Bind b0) u0 (lift (S O) O t5)) H16) in ((let H19 \def 
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
+[(TSort _) \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t7: 
+T) on t7: T \def (match t7 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) 
+\Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false 
+\Rightarrow (f i)])) | (THead k u1 t8) \Rightarrow (THead k (lref_map f d u1) 
+(lref_map f (s k d) t8))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O 
+t3) | (TLRef _) \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) 
+(t7: T) on t7: T \def (match t7 with [(TSort n) \Rightarrow (TSort n) | 
+(TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | 
+false \Rightarrow (f i)])) | (THead k u1 t8) \Rightarrow (THead k (lref_map f 
+d u1) (lref_map f (s k d) t8))]) in lref_map) (\lambda (x: nat).(plus x (S 
+O))) O t3) | (THead _ _ t7) \Rightarrow t7])) (THead (Bind b) u (lift (S O) O 
+t3)) (THead (Bind b0) u0 (lift (S O) O t5)) H16) in (\lambda (_: (eq T u 
+u0)).(\lambda (H21: (eq B b b0)).(let H22 \def (eq_ind_r T t (\lambda (t7: 
 T).(\forall (v: T).((tlt v t7) \to (\forall (t8: T).((pr0 v t8) \to (\forall 
 (t9: T).((pr0 v t9) \to (ex2 T (\lambda (t10: T).(pr0 t8 t10)) (\lambda (t10: 
-T).(pr0 t9 t10)))))))))) H (THead (Flat Cast) u1 t5) H20) in (let H22 \def 
-(eq_ind T t3 (\lambda (t7: T).(pr0 t7 t1)) H6 t5 H17) in (ex2_ind T (\lambda 
-(t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t6 t7)) (ex2 T (\lambda (t7: 
-T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead (Flat Cast) u2 t6) t7))) 
-(\lambda (x: T).(\lambda (H23: (pr0 t1 x)).(\lambda (H24: (pr0 t6 
-x)).(ex_intro2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead 
-(Flat Cast) u2 t6) t7)) x H23 (pr0_epsilon t6 x H24 u2))))) (H21 t5 
-(tlt_head_dx (Flat Cast) u1 t5) t1 H22 t6 H13))))) k H19)))) H16)) H15))))) 
-t2 H11)) t H9 H10 H7 H8))) | (pr0_beta u0 v1 v2 H7 t5 t6 H8) \Rightarrow 
-(\lambda (H9: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)) 
-t)).(\lambda (H10: (eq T (THead (Bind Abbr) v2 t6) t2)).(eq_ind T (THead 
-(Flat Appl) v1 (THead (Bind Abst) u0 t5)) (\lambda (_: T).((eq T (THead (Bind 
-Abbr) v2 t6) t2) \to ((pr0 v1 v2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: 
-T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))) (\lambda (H11: (eq T 
-(THead (Bind Abbr) v2 t6) t2)).(eq_ind T (THead (Bind Abbr) v2 t6) (\lambda 
-(t7: T).((pr0 v1 v2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 
-t8)) (\lambda (t8: T).(pr0 t7 t8)))))) (\lambda (_: (pr0 v1 v2)).(\lambda (_: 
+T).(pr0 t9 t10)))))))))) H (THead (Bind b0) u0 (lift (S O) O t5)) H11) in 
+(let H23 \def (eq_ind T t3 (\lambda (t7: T).(pr0 t7 t1)) H8 t5 (lift_inj t3 
+t5 (S O) O H19)) in (let H24 \def (eq_ind B b (\lambda (b1: B).(not (eq B b1 
+Abst))) H7 b0 H21) in (ex2_ind T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: 
+T).(pr0 t2 t7)) (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 
+t7))) (\lambda (x: T).(\lambda (H25: (pr0 t1 x)).(\lambda (H26: (pr0 t2 
+x)).(ex_intro2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)) 
+x H25 H26)))) (H22 t5 (lift_tlt_dx (Bind b0) u0 t5 (S O) O) t1 H23 t2 
+H15)))))))) H18)) H17))))) t6 (sym_eq T t6 t2 H13))) t H11 H12 H9 H10))) | 
+(pr0_tau t5 t6 H9 u0) \Rightarrow (\lambda (H10: (eq T (THead (Flat Cast) u0 
+t5) t)).(\lambda (H11: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u0 t5) 
+(\lambda (_: T).((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: 
+T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H12: (eq T t6 
+t2)).(eq_ind T t2 (\lambda (t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8: 
+T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))) (\lambda (_: (pr0 t5 
+t2)).(let H14 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Bind b) u 
+(lift (S O) O t3)) t7)) H4 (THead (Flat Cast) u0 t5) H10) in (let H15 \def 
+(eq_ind T (THead (Bind b) u (lift (S O) O t3)) (\lambda (ee: T).(match ee in 
+T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
+(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
+False])])) I (THead (Flat Cast) u0 t5) H14) in (False_ind (ex2 T (\lambda 
+(t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7))) H15)))) t6 (sym_eq T t6 
+t2 H12))) t H10 H11 H9)))]) in (H9 (refl_equal T t) (refl_equal T t2))))) t4 
+(sym_eq T t4 t1 H6))) t H4 H5 H2 H3))) | (pr0_tau t3 t4 H2 u) \Rightarrow 
+(\lambda (H3: (eq T (THead (Flat Cast) u t3) t)).(\lambda (H4: (eq T t4 
+t1)).(eq_ind T (THead (Flat Cast) u t3) (\lambda (_: T).((eq T t4 t1) \to 
+((pr0 t3 t4) \to (ex2 T (\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 
+t2 t6)))))) (\lambda (H5: (eq T t4 t1)).(eq_ind T t1 (\lambda (t5: T).((pr0 
+t3 t5) \to (ex2 T (\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 t2 
+t6))))) (\lambda (H6: (pr0 t3 t1)).(let H7 \def (match H1 in pr0 return 
+(\lambda (t5: T).(\lambda (t6: T).(\lambda (_: (pr0 t5 t6)).((eq T t5 t) \to 
+((eq T t6 t2) \to (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 
+t2 t7)))))))) with [(pr0_refl t5) \Rightarrow (\lambda (H7: (eq T t5 
+t)).(\lambda (H8: (eq T t5 t2)).(eq_ind T t (\lambda (t6: T).((eq T t6 t2) 
+\to (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7))))) 
+(\lambda (H9: (eq T t t2)).(eq_ind T t2 (\lambda (_: T).(ex2 T (\lambda (t7: 
+T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)))) (let H10 \def (eq_ind_r T t 
+(\lambda (t6: T).(eq T t6 t2)) H9 (THead (Flat Cast) u t3) H3) in (eq_ind T 
+(THead (Flat Cast) u t3) (\lambda (t6: T).(ex2 T (\lambda (t7: T).(pr0 t1 
+t7)) (\lambda (t7: T).(pr0 t6 t7)))) (let H11 \def (eq_ind_r T t (\lambda 
+(t6: T).(eq T t5 t6)) H7 (THead (Flat Cast) u t3) H3) in (let H12 \def 
+(eq_ind_r T t (\lambda (t6: T).(\forall (v: T).((tlt v t6) \to (\forall (t7: 
+T).((pr0 v t7) \to (\forall (t8: T).((pr0 v t8) \to (ex2 T (\lambda (t9: 
+T).(pr0 t7 t9)) (\lambda (t9: T).(pr0 t8 t9)))))))))) H (THead (Flat Cast) u 
+t3) H3) in (ex_intro2 T (\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 
+(THead (Flat Cast) u t3) t6)) t1 (pr0_refl t1) (pr0_tau t3 t1 H6 u)))) t2 
+H10)) t (sym_eq T t t2 H9))) t5 (sym_eq T t5 t H7) H8))) | (pr0_comp u1 u2 H7 
+t5 t6 H8 k) \Rightarrow (\lambda (H9: (eq T (THead k u1 t5) t)).(\lambda 
+(H10: (eq T (THead k u2 t6) t2)).(eq_ind T (THead k u1 t5) (\lambda (_: 
+T).((eq T (THead k u2 t6) t2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T 
+(\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))) (\lambda 
+(H11: (eq T (THead k u2 t6) t2)).(eq_ind T (THead k u2 t6) (\lambda (t7: 
+T).((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) 
+(\lambda (t8: T).(pr0 t7 t8)))))) (\lambda (_: (pr0 u1 u2)).(\lambda (H13: 
 (pr0 t5 t6)).(let H14 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat 
-Cast) u t3) t7)) H3 (THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)) H9) in 
-(let H15 \def (eq_ind T (THead (Flat Cast) u t3) (\lambda (ee: T).(match ee 
-in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef 
-_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow 
-(match f in F return (\lambda (_: F).Prop) with [Appl \Rightarrow False | 
-Cast \Rightarrow True])])])) I (THead (Flat Appl) v1 (THead (Bind Abst) u0 
-t5)) H14) in (False_ind (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: 
-T).(pr0 (THead (Bind Abbr) v2 t6) t7))) H15))))) t2 H11)) t H9 H10 H7 H8))) | 
-(pr0_upsilon b H7 v1 v2 H8 u1 u2 H9 t5 t6 H10) \Rightarrow (\lambda (H11: (eq 
-T (THead (Flat Appl) v1 (THead (Bind b) u1 t5)) t)).(\lambda (H12: (eq T 
-(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T 
-(THead (Flat Appl) v1 (THead (Bind b) u1 t5)) (\lambda (_: T).((eq T (THead 
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t2) \to ((not (eq B b 
-Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda 
-(t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) (\lambda (H13: (eq 
-T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T 
-(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) (\lambda (t7: 
-T).((not (eq B b Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) 
-\to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t7 t8)))))))) 
-(\lambda (_: (not (eq B b Abst))).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (pr0 
-u1 u2)).(\lambda (_: (pr0 t5 t6)).(let H18 \def (eq_ind_r T t (\lambda (t7: 
+Cast) u t3) t7)) H3 (THead k u1 t5) H9) in (let H15 \def (f_equal T K 
+(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) 
+\Rightarrow (Flat Cast) | (TLRef _) \Rightarrow (Flat Cast) | (THead k0 _ _) 
+\Rightarrow k0])) (THead (Flat Cast) u t3) (THead k u1 t5) H14) in ((let H16 
+\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
+with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t7 _) 
+\Rightarrow t7])) (THead (Flat Cast) u t3) (THead k u1 t5) H14) in ((let H17 
+\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
+with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t7) 
+\Rightarrow t7])) (THead (Flat Cast) u t3) (THead k u1 t5) H14) in (\lambda 
+(_: (eq T u u1)).(\lambda (H19: (eq K (Flat Cast) k)).(eq_ind K (Flat Cast) 
+(\lambda (k0: K).(ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 
+(THead k0 u2 t6) t7)))) (let H20 \def (eq_ind_r K k (\lambda (k0: K).(eq T 
+(THead k0 u1 t5) t)) H9 (Flat Cast) H19) in (let H21 \def (eq_ind_r T t 
+(\lambda (t7: T).(\forall (v: T).((tlt v t7) \to (\forall (t8: T).((pr0 v t8) 
+\to (\forall (t9: T).((pr0 v t9) \to (ex2 T (\lambda (t10: T).(pr0 t8 t10)) 
+(\lambda (t10: T).(pr0 t9 t10)))))))))) H (THead (Flat Cast) u1 t5) H20) in 
+(let H22 \def (eq_ind T t3 (\lambda (t7: T).(pr0 t7 t1)) H6 t5 H17) in 
+(ex2_ind T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t6 t7)) (ex2 T 
+(\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead (Flat Cast) u2 t6) 
+t7))) (\lambda (x: T).(\lambda (H23: (pr0 t1 x)).(\lambda (H24: (pr0 t6 
+x)).(ex_intro2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead 
+(Flat Cast) u2 t6) t7)) x H23 (pr0_tau t6 x H24 u2))))) (H21 t5 (tlt_head_dx 
+(Flat Cast) u1 t5) t1 H22 t6 H13))))) k H19)))) H16)) H15))))) t2 H11)) t H9 
+H10 H7 H8))) | (pr0_beta u0 v1 v2 H7 t5 t6 H8) \Rightarrow (\lambda (H9: (eq 
+T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)) t)).(\lambda (H10: (eq T 
+(THead (Bind Abbr) v2 t6) t2)).(eq_ind T (THead (Flat Appl) v1 (THead (Bind 
+Abst) u0 t5)) (\lambda (_: T).((eq T (THead (Bind Abbr) v2 t6) t2) \to ((pr0 
+v1 v2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda 
+(t8: T).(pr0 t2 t8))))))) (\lambda (H11: (eq T (THead (Bind Abbr) v2 t6) 
+t2)).(eq_ind T (THead (Bind Abbr) v2 t6) (\lambda (t7: T).((pr0 v1 v2) \to 
+((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 
+t7 t8)))))) (\lambda (_: (pr0 v1 v2)).(\lambda (_: (pr0 t5 t6)).(let H14 \def 
+(eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Cast) u t3) t7)) H3 (THead 
+(Flat Appl) v1 (THead (Bind Abst) u0 t5)) H9) in (let H15 \def (eq_ind T 
+(THead (Flat Cast) u t3) (\lambda (ee: T).(match ee in T return (\lambda (_: 
+T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
+(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
+[(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f in F return 
+(\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast \Rightarrow 
+True])])])) I (THead (Flat Appl) v1 (THead (Bind Abst) u0 t5)) H14) in 
+(False_ind (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 (THead 
+(Bind Abbr) v2 t6) t7))) H15))))) t2 H11)) t H9 H10 H7 H8))) | (pr0_upsilon b 
+H7 v1 v2 H8 u1 u2 H9 t5 t6 H10) \Rightarrow (\lambda (H11: (eq T (THead (Flat 
+Appl) v1 (THead (Bind b) u1 t5)) t)).(\lambda (H12: (eq T (THead (Bind b) u2 
+(THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T (THead (Flat Appl) 
+v1 (THead (Bind b) u1 t5)) (\lambda (_: T).((eq T (THead (Bind b) u2 (THead 
+(Flat Appl) (lift (S O) O v2) t6)) t2) \to ((not (eq B b Abst)) \to ((pr0 v1 
+v2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 
+t8)) (\lambda (t8: T).(pr0 t2 t8))))))))) (\lambda (H13: (eq T (THead (Bind 
+b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t2)).(eq_ind T (THead (Bind 
+b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) (\lambda (t7: T).((not (eq B 
+b Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ex2 T 
+(\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: T).(pr0 t7 t8)))))))) (\lambda 
+(_: (not (eq B b Abst))).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (pr0 u1 
+u2)).(\lambda (_: (pr0 t5 t6)).(let H18 \def (eq_ind_r T t (\lambda (t7: 
 T).(eq T (THead (Flat Cast) u t3) t7)) H3 (THead (Flat Appl) v1 (THead (Bind 
 b) u1 t5)) H11) in (let H19 \def (eq_ind T (THead (Flat Cast) u t3) (\lambda 
 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
@@ -2451,31 +2450,31 @@ False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
 \Rightarrow True])])) I (THead (Bind b) u0 (lift (S O) O t5)) H14) in 
 (False_ind (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 
-t7))) H15))))) t6 (sym_eq T t6 t2 H11))) t H9 H10 H7 H8))) | (pr0_epsilon t5 
-t6 H7 u0) \Rightarrow (\lambda (H8: (eq T (THead (Flat Cast) u0 t5) 
-t)).(\lambda (H9: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u0 t5) (\lambda 
-(_: T).((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 
-t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H10: (eq T t6 t2)).(eq_ind T 
-t2 (\lambda (t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) 
-(\lambda (t8: T).(pr0 t2 t8))))) (\lambda (H11: (pr0 t5 t2)).(let H12 \def 
-(eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Cast) u t3) t7)) H3 (THead 
-(Flat Cast) u0 t5) H8) in (let H13 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) 
-\Rightarrow u | (THead _ t7 _) \Rightarrow t7])) (THead (Flat Cast) u t3) 
-(THead (Flat Cast) u0 t5) H12) in ((let H14 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | 
-(TLRef _) \Rightarrow t3 | (THead _ _ t7) \Rightarrow t7])) (THead (Flat 
-Cast) u t3) (THead (Flat Cast) u0 t5) H12) in (\lambda (_: (eq T u u0)).(let 
-H16 \def (eq_ind_r T t (\lambda (t7: T).(\forall (v: T).((tlt v t7) \to 
-(\forall (t8: T).((pr0 v t8) \to (\forall (t9: T).((pr0 v t9) \to (ex2 T 
-(\lambda (t10: T).(pr0 t8 t10)) (\lambda (t10: T).(pr0 t9 t10)))))))))) H 
-(THead (Flat Cast) u0 t5) H8) in (let H17 \def (eq_ind T t3 (\lambda (t7: 
-T).(pr0 t7 t1)) H6 t5 H14) in (ex2_ind T (\lambda (t7: T).(pr0 t1 t7)) 
-(\lambda (t7: T).(pr0 t2 t7)) (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda 
-(t7: T).(pr0 t2 t7))) (\lambda (x: T).(\lambda (H18: (pr0 t1 x)).(\lambda 
-(H19: (pr0 t2 x)).(ex_intro2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: 
-T).(pr0 t2 t7)) x H18 H19)))) (H16 t5 (tlt_head_dx (Flat Cast) u0 t5) t1 H17 
-t2 H11)))))) H13)))) t6 (sym_eq T t6 t2 H10))) t H8 H9 H7)))]) in (H7 
-(refl_equal T t) (refl_equal T t2)))) t4 (sym_eq T t4 t1 H5))) t H3 H4 
-H2)))]) in (H2 (refl_equal T t) (refl_equal T t1))))))))) t0).
+t7))) H15))))) t6 (sym_eq T t6 t2 H11))) t H9 H10 H7 H8))) | (pr0_tau t5 t6 
+H7 u0) \Rightarrow (\lambda (H8: (eq T (THead (Flat Cast) u0 t5) t)).(\lambda 
+(H9: (eq T t6 t2)).(eq_ind T (THead (Flat Cast) u0 t5) (\lambda (_: T).((eq T 
+t6 t2) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda 
+(t8: T).(pr0 t2 t8)))))) (\lambda (H10: (eq T t6 t2)).(eq_ind T t2 (\lambda 
+(t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8: T).(pr0 t1 t8)) (\lambda (t8: 
+T).(pr0 t2 t8))))) (\lambda (H11: (pr0 t5 t2)).(let H12 \def (eq_ind_r T t 
+(\lambda (t7: T).(eq T (THead (Flat Cast) u t3) t7)) H3 (THead (Flat Cast) u0 
+t5) H8) in (let H13 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | 
+(THead _ t7 _) \Rightarrow t7])) (THead (Flat Cast) u t3) (THead (Flat Cast) 
+u0 t5) H12) in ((let H14 \def (f_equal T T (\lambda (e: T).(match e in T 
+return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) 
+\Rightarrow t3 | (THead _ _ t7) \Rightarrow t7])) (THead (Flat Cast) u t3) 
+(THead (Flat Cast) u0 t5) H12) in (\lambda (_: (eq T u u0)).(let H16 \def 
+(eq_ind_r T t (\lambda (t7: T).(\forall (v: T).((tlt v t7) \to (\forall (t8: 
+T).((pr0 v t8) \to (\forall (t9: T).((pr0 v t9) \to (ex2 T (\lambda (t10: 
+T).(pr0 t8 t10)) (\lambda (t10: T).(pr0 t9 t10)))))))))) H (THead (Flat Cast) 
+u0 t5) H8) in (let H17 \def (eq_ind T t3 (\lambda (t7: T).(pr0 t7 t1)) H6 t5 
+H14) in (ex2_ind T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 
+t7)) (ex2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7))) 
+(\lambda (x: T).(\lambda (H18: (pr0 t1 x)).(\lambda (H19: (pr0 t2 
+x)).(ex_intro2 T (\lambda (t7: T).(pr0 t1 t7)) (\lambda (t7: T).(pr0 t2 t7)) 
+x H18 H19)))) (H16 t5 (tlt_head_dx (Flat Cast) u0 t5) t1 H17 t2 H11)))))) 
+H13)))) t6 (sym_eq T t6 t2 H10))) t H8 H9 H7)))]) in (H7 (refl_equal T t) 
+(refl_equal T t2)))) t4 (sym_eq T t4 t1 H5))) t H3 H4 H2)))]) in (H2 
+(refl_equal T t) (refl_equal T t1))))))))) t0).