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
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
(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
(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
(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
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
(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
(_: 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
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
(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
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
(\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 _)
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).