-(Bind Abbr) u0 t5) H16) in (let H23 \def (match H22 in eq return (\lambda
-(t7: T).(\lambda (_: (eq ? ? t7)).((eq T t7 (THead (Bind Abbr) u0 t5)) \to
-(ex2 T (\lambda (t8: T).(pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 (THead (Bind Abbr) u3 w) t8))))))
-with [refl_equal \Rightarrow (\lambda (H23: (eq T (THead (Flat Appl) v1
-(THead (Bind b) u1 t3)) (THead (Bind Abbr) u0 t5))).(let H24 \def (eq_ind T
-(THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (\lambda (e: T).(match e 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 _) \Rightarrow
-True])])) I (THead (Bind Abbr) u0 t5) H23) 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 (THead (Bind Abbr) u3 w) t7))) H24)))]) in (H23
-(refl_equal T (THead (Bind Abbr) u0 t5)))))))) t2 H18)) t H16 H17 H13 H14
-H15))) | (pr0_zeta b0 H13 t5 t6 H14 u) \Rightarrow (\lambda (H15: (eq T
-(THead (Bind b0) u (lift (S O) O t5)) t)).(\lambda (H16: (eq T t6
-t2)).(eq_ind T (THead (Bind b0) u (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 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t8))
-(\lambda (t8: T).(pr0 t2 t8))))))) (\lambda (H17: (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 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (_: (not (eq B b0
-Abst))).(\lambda (_: (pr0 t5 t2)).(let H20 \def (eq_ind_r T t (\lambda (t7:
-T).(eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) t7)) H6 (THead (Bind
-b0) u (lift (S O) O t5)) H15) in (let H21 \def (match H20 in eq return
-(\lambda (t7: T).(\lambda (_: (eq ? ? t7)).((eq T t7 (THead (Bind b0) u (lift
-(S O) O t5))) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2 t8))))))
-with [refl_equal \Rightarrow (\lambda (H21: (eq T (THead (Flat Appl) v1
-(THead (Bind b) u1 t3)) (THead (Bind b0) u (lift (S O) O t5)))).(let H22 \def
-(eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (\lambda (e:
-T).(match e 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 _)
-\Rightarrow True])])) I (THead (Bind b0) u (lift (S O) O t5)) H21) 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))) H22)))]) in (H21
-(refl_equal T (THead (Bind b0) u (lift (S O) O t5)))))))) t6 (sym_eq T t6 t2
-H17))) t H15 H16 H13 H14))) | (pr0_epsilon 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 (THead (Flat Appl) (lift (S
-O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2 t8)))))) (\lambda (H16: (eq T t6
-t2)).(eq_ind T t2 (\lambda (t7: T).((pr0 t5 t7) \to (ex2 T (\lambda (t8:
-T).(pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t8))
-(\lambda (t8: T).(pr0 t2 t8))))) (\lambda (_: (pr0 t5 t2)).(let H18 \def
-(eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Appl) v1 (THead (Bind b) u1
-t3)) t7)) H6 (THead (Flat Cast) u t5) H14) in (let H19 \def (match H18 in eq
-return (\lambda (t7: T).(\lambda (_: (eq ? ? t7)).((eq T t7 (THead (Flat
-Cast) u t5)) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2 t8)))))) with
-[refl_equal \Rightarrow (\lambda (H19: (eq T (THead (Flat Appl) v1 (THead
-(Bind b) u1 t3)) (THead (Flat Cast) u t5))).(let H20 \def (eq_ind T (THead
-(Flat Appl) v1 (THead (Bind b) u1 t3)) (\lambda (e: T).(match e 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 True | Cast
-\Rightarrow False])])])) I (THead (Flat Cast) u t5) H19) 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))) H20)))]) in (H19 (refl_equal T
-(THead (Flat Cast) u t5)))))) t6 (sym_eq T t6 t2 H16))) t H14 H15 H13)))]) in
-(H13 (refl_equal T t) (refl_equal T t2))))))) t1 H8)) t H6 H7 H2 H3 H4 H5)))
-| (pr0_delta u1 u2 H2 t3 t4 H3 w H4) \Rightarrow (\lambda (H5: (eq T (THead
-(Bind Abbr) u1 t3) t)).(\lambda (H6: (eq T (THead (Bind Abbr) u2 w)
-t1)).(eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (_: T).((eq T (THead (Bind
-Abbr) u2 w) t1) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to ((subst0 O u2 t4 w) \to
-(ex2 T (\lambda (t6: T).(pr0 t1 t6)) (\lambda (t6: T).(pr0 t2 t6))))))))
-(\lambda (H7: (eq T (THead (Bind Abbr) u2 w) t1)).(eq_ind T (THead (Bind
-Abbr) u2 w) (\lambda (t5: T).((pr0 u1 u2) \to ((pr0 t3 t4) \to ((subst0 O u2
-t4 w) \to (ex2 T (\lambda (t6: T).(pr0 t5 t6)) (\lambda (t6: T).(pr0 t2
-t6))))))) (\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (pr0 t3 t4)).(\lambda
-(H10: (subst0 O u2 t4 w)).(let H11 \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 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7:
-T).(pr0 t2 t7)))))))) with [(pr0_refl t5) \Rightarrow (\lambda (H11: (eq T t5
-t)).(\lambda (H12: (eq T t5 t2)).(eq_ind T t (\lambda (t6: T).((eq T t6 t2)
-\to (ex2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7:
-T).(pr0 t2 t7))))) (\lambda (H13: (eq T t t2)).(eq_ind T t2 (\lambda (_:
-T).(ex2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7:
-T).(pr0 t2 t7)))) (let H14 \def (eq_ind_r T t (\lambda (t6: T).(eq T t6 t2))
-H13 (THead (Bind Abbr) u1 t3) H5) in (eq_ind T (THead (Bind Abbr) u1 t3)
-(\lambda (t6: T).(ex2 T (\lambda (t7: T).(pr0 (THead (Bind Abbr) u2 w) t7))
-(\lambda (t7: T).(pr0 t6 t7)))) (let H15 \def (eq_ind_r T t (\lambda (t6:
-T).(eq T t5 t6)) H11 (THead (Bind Abbr) u1 t3) H5) in (let H16 \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 (Bind Abbr) u1 t3) H5) in
-(ex_intro2 T (\lambda (t6: T).(pr0 (THead (Bind Abbr) u2 w) t6)) (\lambda
-(t6: T).(pr0 (THead (Bind Abbr) u1 t3) t6)) (THead (Bind Abbr) u2 w)
-(pr0_refl (THead (Bind Abbr) u2 w)) (pr0_delta u1 u2 H8 t3 t4 H9 w H10)))) t2
-H14)) t (sym_eq T t t2 H13))) t5 (sym_eq T t5 t H11) H12))) | (pr0_comp u0 u3
-H11 t5 t6 H12 k) \Rightarrow (\lambda (H13: (eq T (THead k u0 t5)
-t)).(\lambda (H14: (eq T (THead k u3 t6) t2)).(eq_ind T (THead k u0 t5)
-(\lambda (_: T).((eq T (THead k u3 t6) t2) \to ((pr0 u0 u3) \to ((pr0 t5 t6)
-\to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) u2 w) t8)) (\lambda (t8:
-T).(pr0 t2 t8))))))) (\lambda (H15: (eq T (THead k u3 t6) t2)).(eq_ind T
-(THead k u3 t6) (\lambda (t7: T).((pr0 u0 u3) \to ((pr0 t5 t6) \to (ex2 T
-(\lambda (t8: T).(pr0 (THead (Bind Abbr) u2 w) t8)) (\lambda (t8: T).(pr0 t7
-t8)))))) (\lambda (H16: (pr0 u0 u3)).(\lambda (H17: (pr0 t5 t6)).(let H18
-\def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Bind Abbr) u1 t3) t7)) H5
-(THead k u0 t5) H13) in (let H19 \def (match H18 in eq return (\lambda (t7:
-T).(\lambda (_: (eq ? ? t7)).((eq T t7 (THead k u0 t5)) \to (ex2 T (\lambda
-(t8: T).(pr0 (THead (Bind Abbr) u2 w) t8)) (\lambda (t8: T).(pr0 (THead k u3
-t6) t8)))))) with [refl_equal \Rightarrow (\lambda (H19: (eq T (THead (Bind
-Abbr) u1 t3) (THead k u0 t5))).(let H20 \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 (Bind
-Abbr) u1 t3) (THead k u0 t5) H19) in ((let H21 \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 (Bind
-Abbr) u1 t3) (THead k u0 t5) H19) in ((let H22 \def (f_equal T K (\lambda (e:
-T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow (Bind
-Abbr) | (TLRef _) \Rightarrow (Bind Abbr) | (THead k0 _ _) \Rightarrow k0]))
-(THead (Bind Abbr) u1 t3) (THead k u0 t5) H19) in (eq_ind K (Bind Abbr)
-(\lambda (k0: K).((eq T u1 u0) \to ((eq T t3 t5) \to (ex2 T (\lambda (t7:
-T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 (THead k0 u3 t6)
-t7)))))) (\lambda (H23: (eq T u1 u0)).(eq_ind T u0 (\lambda (_: T).((eq T t3
-t5) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind Abbr) u2 w) t8)) (\lambda
-(t8: T).(pr0 (THead (Bind Abbr) u3 t6) t8))))) (\lambda (H24: (eq T t3
-t5)).(eq_ind T t5 (\lambda (_: T).(ex2 T (\lambda (t8: T).(pr0 (THead (Bind
-Abbr) u2 w) t8)) (\lambda (t8: T).(pr0 (THead (Bind Abbr) u3 t6) t8)))) (let
-H25 \def (eq_ind_r K k (\lambda (k0: K).(eq T (THead k0 u0 t5) t)) H13 (Bind
-Abbr) H22) in (let H26 \def (eq_ind_r T t (\lambda (t7: T).(\forall (v:
+(Bind Abbr) u0 t5) H16) in (let H23 \def (eq_ind T (THead (Flat Appl) v1
+(THead (Bind b) u1 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 _) \Rightarrow True])])) I (THead (Bind
+Abbr) u0 t5) H22) 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
+(THead (Bind Abbr) u3 w) t7))) H23)))))) t2 H18)) t H16 H17 H13 H14 H15))) |
+(pr0_zeta b0 H13 t5 t6 H14 u) \Rightarrow (\lambda (H15: (eq T (THead (Bind
+b0) u (lift (S O) O t5)) t)).(\lambda (H16: (eq T t6 t2)).(eq_ind T (THead
+(Bind b0) u (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 (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2
+t8))))))) (\lambda (H17: (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 (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) t8)) (\lambda (t8:
+T).(pr0 t2 t8)))))) (\lambda (_: (not (eq B b0 Abst))).(\lambda (_: (pr0 t5
+t2)).(let H20 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat Appl) v1
+(THead (Bind b) u1 t3)) t7)) H6 (THead (Bind b0) u (lift (S O) O t5)) H15) in
+(let H21 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 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 _) \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_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
+(THead (Flat Appl) (lift (S O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2
+t8)))))) (\lambda (H16: (eq T t6 t2)).(eq_ind T t2 (\lambda (t7: T).((pr0 t5
+t7) \to (ex2 T (\lambda (t8: T).(pr0 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) t8)) (\lambda (t8: T).(pr0 t2 t8))))) (\lambda (_:
+(pr0 t5 t2)).(let H18 \def (eq_ind_r T t (\lambda (t7: T).(eq T (THead (Flat
+Appl) v1 (THead (Bind b) u1 t3)) t7)) H6 (THead (Flat Cast) u t5) H14) in
+(let H19 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 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 True | Cast \Rightarrow False])])])) I (THead (Flat Cast) u t5)
+H18) 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)))
+H19)))) t6 (sym_eq T t6 t2 H16))) t H14 H15 H13)))]) in (H13 (refl_equal T t)
+(refl_equal T t2))))))) t1 H8)) t H6 H7 H2 H3 H4 H5))) | (pr0_delta u1 u2 H2
+t3 t4 H3 w H4) \Rightarrow (\lambda (H5: (eq T (THead (Bind Abbr) u1 t3)
+t)).(\lambda (H6: (eq T (THead (Bind Abbr) u2 w) t1)).(eq_ind T (THead (Bind
+Abbr) u1 t3) (\lambda (_: T).((eq T (THead (Bind Abbr) u2 w) t1) \to ((pr0 u1
+u2) \to ((pr0 t3 t4) \to ((subst0 O u2 t4 w) \to (ex2 T (\lambda (t6: T).(pr0
+t1 t6)) (\lambda (t6: T).(pr0 t2 t6)))))))) (\lambda (H7: (eq T (THead (Bind
+Abbr) u2 w) t1)).(eq_ind T (THead (Bind Abbr) u2 w) (\lambda (t5: T).((pr0 u1
+u2) \to ((pr0 t3 t4) \to ((subst0 O u2 t4 w) \to (ex2 T (\lambda (t6: T).(pr0
+t5 t6)) (\lambda (t6: T).(pr0 t2 t6))))))) (\lambda (H8: (pr0 u1
+u2)).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (subst0 O u2 t4 w)).(let H11
+\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
+(THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 t2 t7)))))))) with
+[(pr0_refl t5) \Rightarrow (\lambda (H11: (eq T t5 t)).(\lambda (H12: (eq T
+t5 t2)).(eq_ind T t (\lambda (t6: T).((eq T t6 t2) \to (ex2 T (\lambda (t7:
+T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 t2 t7)))))
+(\lambda (H13: (eq T t t2)).(eq_ind T t2 (\lambda (_: T).(ex2 T (\lambda (t7:
+T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 t2 t7)))) (let
+H14 \def (eq_ind_r T t (\lambda (t6: T).(eq T t6 t2)) H13 (THead (Bind Abbr)
+u1 t3) H5) in (eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (t6: T).(ex2 T
+(\lambda (t7: T).(pr0 (THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 t6
+t7)))) (let H15 \def (eq_ind_r T t (\lambda (t6: T).(eq T t5 t6)) H11 (THead
+(Bind Abbr) u1 t3) H5) in (let H16 \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 (Bind Abbr) u1 t3) H5) in (ex_intro2 T
+(\lambda (t6: T).(pr0 (THead (Bind Abbr) u2 w) t6)) (\lambda (t6: T).(pr0
+(THead (Bind Abbr) u1 t3) t6)) (THead (Bind Abbr) u2 w) (pr0_refl (THead
+(Bind Abbr) u2 w)) (pr0_delta u1 u2 H8 t3 t4 H9 w H10)))) t2 H14)) t (sym_eq
+T t t2 H13))) t5 (sym_eq T t5 t H11) H12))) | (pr0_comp u0 u3 H11 t5 t6 H12
+k) \Rightarrow (\lambda (H13: (eq T (THead k u0 t5) t)).(\lambda (H14: (eq T
+(THead k u3 t6) t2)).(eq_ind T (THead k u0 t5) (\lambda (_: T).((eq T (THead
+k u3 t6) t2) \to ((pr0 u0 u3) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8:
+T).(pr0 (THead (Bind Abbr) u2 w) t8)) (\lambda (t8: T).(pr0 t2 t8)))))))
+(\lambda (H15: (eq T (THead k u3 t6) t2)).(eq_ind T (THead k u3 t6) (\lambda
+(t7: T).((pr0 u0 u3) \to ((pr0 t5 t6) \to (ex2 T (\lambda (t8: T).(pr0 (THead
+(Bind Abbr) u2 w) t8)) (\lambda (t8: T).(pr0 t7 t8)))))) (\lambda (H16: (pr0
+u0 u3)).(\lambda (H17: (pr0 t5 t6)).(let H18 \def (eq_ind_r T t (\lambda (t7:
+T).(eq T (THead (Bind Abbr) u1 t3) t7)) H5 (THead k u0 t5) H13) in (let H19
+\def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
+with [(TSort _) \Rightarrow (Bind Abbr) | (TLRef _) \Rightarrow (Bind Abbr) |
+(THead k0 _ _) \Rightarrow k0])) (THead (Bind Abbr) u1 t3) (THead k u0 t5)
+H18) in ((let H20 \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 (Bind Abbr) u1 t3) (THead k u0 t5)
+H18) in ((let H21 \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 (Bind Abbr) u1 t3) (THead k u0 t5)
+H18) in (\lambda (H22: (eq T u1 u0)).(\lambda (H23: (eq K (Bind Abbr)
+k)).(eq_ind K (Bind Abbr) (\lambda (k0: K).(ex2 T (\lambda (t7: T).(pr0
+(THead (Bind Abbr) u2 w) t7)) (\lambda (t7: T).(pr0 (THead k0 u3 t6) t7))))
+(let H24 \def (eq_ind_r K k (\lambda (k0: K).(eq T (THead k0 u0 t5) t)) H13
+(Bind Abbr) H23) in (let H25 \def (eq_ind_r T t (\lambda (t7: T).(\forall (v: