-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: