-(H34: (eq T t8 t4)).(eq_ind T t4 (\lambda (t9: T).((not (eq B Abst Abst)) \to
-((pr0 t7 t9) \to (ex2 T (\lambda (t10: T).(pr0 (THead (Flat Appl) u2 t4)
-t10)) (\lambda (t10: T).(pr0 (THead (Bind Abbr) v2 t6) t10)))))) (\lambda
-(H35: (not (eq B Abst Abst))).(\lambda (_: (pr0 t7 t4)).(let H37 \def (match
-(H35 (refl_equal B Abst)) in False return (\lambda (_: False).(ex2 T (\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_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
-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:
-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
-t7 (THead (Bind b) u0 t5)) \to ((eq T t8 t4) \to (ex2 T (\lambda (t9: T).(pr0
-(THead (Flat Appl) u2 t4) t9)) (\lambda (t9: T).(pr0 (THead (Bind b) u3
-(THead (Flat Appl) (lift (S O) O v2) t6)) t9)))))))) with [(pr0_refl t7)
-\Rightarrow (\lambda (H29: (eq T t7 (THead (Bind b) u0 t5))).(\lambda (H30:
-(eq T t7 t4)).(eq_ind T (THead (Bind b) u0 t5) (\lambda (t8: T).((eq T t8 t4)
-\to (ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t4) t9)) (\lambda (t9:
-T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) t9)))))
-(\lambda (H31: (eq T (THead (Bind b) u0 t5) t4)).(eq_ind T (THead (Bind b) u0
-t5) (\lambda (t8: T).(ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t8)
-t9)) (\lambda (t9: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O)
-O v2) t6)) t9)))) (ex2_ind T (\lambda (t8: T).(pr0 u2 t8)) (\lambda (t8:
-T).(pr0 v2 t8)) (ex2 T (\lambda (t8: T).(pr0 (THead (Flat Appl) u2 (THead
-(Bind b) u0 t5)) t8)) (\lambda (t8: T).(pr0 (THead (Bind b) u3 (THead (Flat
-Appl) (lift (S O) O v2) t6)) t8))) (\lambda (x: T).(\lambda (H32: (pr0 u2
-x)).(\lambda (H33: (pr0 v2 x)).(pr0_confluence__pr0_cong_upsilon_refl b H16
-u0 u3 H18 t5 t6 H19 u2 v2 x H32 H33)))) (H26 v1 (tlt_head_sx (Flat Appl) v1
-(THead (Bind b) u0 t5)) u2 H27 v2 H17)) t4 H31)) t7 (sym_eq T t7 (THead (Bind
-b) u0 t5) H29) H30))) | (pr0_comp u4 u5 H29 t7 t8 H30 k0) \Rightarrow
-(\lambda (H31: (eq T (THead k0 u4 t7) (THead (Bind b) u0 t5))).(\lambda (H32:
-(eq T (THead k0 u5 t8) t4)).((let H33 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t7 |
-(TLRef _) \Rightarrow t7 | (THead _ _ t9) \Rightarrow t9])) (THead k0 u4 t7)
-(THead (Bind b) u0 t5) H31) in ((let H34 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u4 |
-(TLRef _) \Rightarrow u4 | (THead _ t9 _) \Rightarrow t9])) (THead k0 u4 t7)
-(THead (Bind b) u0 t5) H31) in ((let H35 \def (f_equal T K (\lambda (e:
-T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k0 |
-(TLRef _) \Rightarrow k0 | (THead k1 _ _) \Rightarrow k1])) (THead k0 u4 t7)
-(THead (Bind b) u0 t5) H31) in (eq_ind K (Bind b) (\lambda (k1: K).((eq T u4
-u0) \to ((eq T t7 t5) \to ((eq T (THead k1 u5 t8) t4) \to ((pr0 u4 u5) \to
-((pr0 t7 t8) \to (ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 t4) t9))
-(\lambda (t9: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2)
-t6)) t9))))))))) (\lambda (H36: (eq T u4 u0)).(eq_ind T u0 (\lambda (t9:
-T).((eq T t7 t5) \to ((eq T (THead (Bind b) u5 t8) t4) \to ((pr0 t9 u5) \to
-((pr0 t7 t8) \to (ex2 T (\lambda (t10: T).(pr0 (THead (Flat Appl) u2 t4)
-t10)) (\lambda (t10: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S
-O) O v2) t6)) t10)))))))) (\lambda (H37: (eq T t7 t5)).(eq_ind T t5 (\lambda
-(t9: T).((eq T (THead (Bind b) u5 t8) t4) \to ((pr0 u0 u5) \to ((pr0 t9 t8)
-\to (ex2 T (\lambda (t10: T).(pr0 (THead (Flat Appl) u2 t4) t10)) (\lambda
-(t10: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6))
-t10))))))) (\lambda (H38: (eq T (THead (Bind b) u5 t8) t4)).(eq_ind T (THead
-(Bind b) u5 t8) (\lambda (t9: T).((pr0 u0 u5) \to ((pr0 t5 t8) \to (ex2 T
-(\lambda (t10: T).(pr0 (THead (Flat Appl) u2 t9) t10)) (\lambda (t10: T).(pr0
-(THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) t10))))))
-(\lambda (H39: (pr0 u0 u5)).(\lambda (H40: (pr0 t5 t8)).(ex2_ind T (\lambda
-(t9: T).(pr0 t8 t9)) (\lambda (t9: T).(pr0 t6 t9)) (ex2 T (\lambda (t9:
-T).(pr0 (THead (Flat Appl) u2 (THead (Bind b) u5 t8)) t9)) (\lambda (t9:
-T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v2) t6)) t9)))
-(\lambda (x: T).(\lambda (H41: (pr0 t8 x)).(\lambda (H42: (pr0 t6
-x)).(ex2_ind T (\lambda (t9: T).(pr0 u5 t9)) (\lambda (t9: T).(pr0 u3 t9))
-(ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 (THead (Bind b) u5 t8))
-t9)) (\lambda (t9: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (S O)
-O v2) t6)) t9))) (\lambda (x0: T).(\lambda (H43: (pr0 u5 x0)).(\lambda (H44:
-(pr0 u3 x0)).(ex2_ind T (\lambda (t9: T).(pr0 u2 t9)) (\lambda (t9: T).(pr0
-v2 t9)) (ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 (THead (Bind b) u5
-t8)) t9)) (\lambda (t9: T).(pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift
-(S O) O v2) t6)) t9))) (\lambda (x1: T).(\lambda (H45: (pr0 u2 x1)).(\lambda
-(H46: (pr0 v2 x1)).(pr0_confluence__pr0_cong_upsilon_cong b H16 u2 v2 x1 H45
-H46 t8 t6 x H41 H42 u5 u3 x0 H43 H44)))) (H26 v1 (tlt_head_sx (Flat Appl) v1
-(THead (Bind b) u0 t5)) u2 H27 v2 H17))))) (H26 u0 (tlt_trans (THead (Bind b)
-u0 t5) u0 (THead (Flat Appl) v1 (THead (Bind b) u0 t5)) (tlt_head_sx (Bind b)
-u0 t5) (tlt_head_dx (Flat Appl) v1 (THead (Bind b) u0 t5))) u5 H39 u3
-H18))))) (H26 t5 (tlt_trans (THead (Bind b) u0 t5) t5 (THead (Flat Appl) v1
-(THead (Bind b) u0 t5)) (tlt_head_dx (Bind b) u0 t5) (tlt_head_dx (Flat Appl)
-v1 (THead (Bind b) u0 t5))) t8 H40 t6 H19)))) t4 H38)) t7 (sym_eq T t7 t5
-H37))) u4 (sym_eq T u4 u0 H36))) k0 (sym_eq K k0 (Bind b) H35))) H34)) H33))
-H32 H29 H30))) | (pr0_beta u v0 v3 H29 t7 t8 H30) \Rightarrow (\lambda (H31:
-(eq T (THead (Flat Appl) v0 (THead (Bind Abst) u t7)) (THead (Bind b) u0
-t5))).(\lambda (H32: (eq T (THead (Bind Abbr) v3 t8) t4)).((let H33 \def
-(eq_ind T (THead (Flat Appl) v0 (THead (Bind Abst) 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) u0 t5) H31) in (False_ind ((eq T
-(THead (Bind Abbr) v3 t8) t4) \to ((pr0 v0 v3) \to ((pr0 t7 t8) \to (ex2 T
+(H34: (eq T (THead (Bind Abst) u3 t8) t4)).(eq_ind T (THead (Bind Abst) u3
+t8) (\lambda (t9: T).((pr0 u u3) \to ((pr0 t5 t8) \to (ex2 T (\lambda (t10:
+T).(pr0 (THead (Flat Appl) u2 t9) t10)) (\lambda (t10: T).(pr0 (THead (Bind
+Abbr) v2 t6) t10)))))) (\lambda (_: (pr0 u u3)).(\lambda (H36: (pr0 t5
+t8)).(ex2_ind T (\lambda (t9: T).(pr0 t8 t9)) (\lambda (t9: T).(pr0 t6 t9))
+(ex2 T (\lambda (t9: T).(pr0 (THead (Flat Appl) u2 (THead (Bind Abst) u3 t8))
+t9)) (\lambda (t9: T).(pr0 (THead (Bind Abbr) v2 t6) t9))) (\lambda (x:
+T).(\lambda (H37: (pr0 t8 x)).(\lambda (H38: (pr0 t6 x)).(ex2_ind T (\lambda
+(t9: T).(pr0 u2 t9)) (\lambda (t9: T).(pr0 v2 t9)) (ex2 T (\lambda (t9:
+T).(pr0 (THead (Flat Appl) u2 (THead (Bind Abst) u3 t8)) t9)) (\lambda (t9:
+T).(pr0 (THead (Bind Abbr) v2 t6) t9))) (\lambda (x0: T).(\lambda (H39: (pr0
+u2 x0)).(\lambda (H40: (pr0 v2 x0)).(ex_intro2 T (\lambda (t9: T).(pr0 (THead
+(Flat Appl) u2 (THead (Bind Abst) u3 t8)) t9)) (\lambda (t9: T).(pr0 (THead
+(Bind Abbr) v2 t6) t9)) (THead (Bind Abbr) x0 x) (pr0_beta u3 u2 x0 H39 t8 x
+H37) (pr0_comp v2 x0 H40 t6 x H38 (Bind Abbr)))))) (H22 v1 (tlt_head_sx (Flat
+Appl) v1 (THead (Bind Abst) u t5)) u2 H23 v2 H14))))) (H22 t5 (tlt_trans
+(THead (Bind Abst) u t5) t5 (THead (Flat Appl) v1 (THead (Bind Abst) u t5))
+(tlt_head_dx (Bind Abst) u t5) (tlt_head_dx (Flat Appl) v1 (THead (Bind Abst)
+u t5))) t8 H36 t6 H15)))) t4 H34)) t7 (sym_eq T t7 t5 H33))) u0 (sym_eq T u0
+u H32))) k0 (sym_eq K k0 (Bind Abst) H31))) H30)) H29)) H28 H25 H26))) |
+(pr0_beta u0 v0 v3 H25 t7 t8 H26) \Rightarrow (\lambda (H27: (eq T (THead
+(Flat Appl) v0 (THead (Bind Abst) u0 t7)) (THead (Bind Abst) u t5))).(\lambda
+(H28: (eq T (THead (Bind Abbr) v3 t8) t4)).((let H29 \def (eq_ind T (THead
+(Flat Appl) v0 (THead (Bind Abst) u0 t7)) (\lambda (e: T).(match e with
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _ _)
+\Rightarrow (match k0 with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
+True])])) I (THead (Bind Abst) u t5) H27) in (False_ind ((eq T (THead (Bind
+Abbr) v3 t8) t4) \to ((pr0 v0 v3) \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)))))) H29)) H28 H25 H26))) | (pr0_upsilon b H25 v0 v3 H26 u0
+u3 H27 t7 t8 H28) \Rightarrow (\lambda (H29: (eq T (THead (Flat Appl) v0
+(THead (Bind b) u0 t7)) (THead (Bind Abst) u t5))).(\lambda (H30: (eq T
+(THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v3) t8)) t4)).((let H31
+\def (eq_ind T (THead (Flat Appl) v0 (THead (Bind b) u0 t7)) (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
+(THead k0 _ _) \Rightarrow (match k0 with [(Bind _) \Rightarrow False | (Flat
+_) \Rightarrow True])])) I (THead (Bind Abst) u t5) H29) in (False_ind ((eq T
+(THead (Bind b) u3 (THead (Flat Appl) (lift (S O) O v3) t8)) t4) \to ((not
+(eq B b Abst)) \to ((pr0 v0 v3) \to ((pr0 u0 u3) \to ((pr0 t7 t8) \to (ex2 T