-False])])) I (THead (Flat Appl) w v) H8) in (False_ind ((eq T t4 t2) \to
-((not (eq B b Abst)) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w
-(THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) | (pr0_epsilon t3 t4 H6 u0)
-\Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl)
-w v))).(\lambda (H8: (eq T t4 t2)).((let H9 \def (eq_ind T (THead (Flat Cast)
-u0 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 False | Cast \Rightarrow True])])])) I (THead
-(Flat Appl) w v) H7) in (False_ind ((eq T t4 t2) \to ((pr0 t3 t4) \to (ty3 g
-c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))) H9)) H8 H6)))]) in
-(H6 (refl_equal T (THead (Flat Appl) w v)) (refl_equal T t2))))))))))))))))
-(\lambda (c: C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t2
-t3)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t4: T).((pr0
-t2 t4) \to (ty3 g c2 t4 t3))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c t3
-t0)).(\lambda (H3: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t4: T).((pr0
-t3 t4) \to (ty3 g c2 t4 t0))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c
-c2)).(\lambda (t4: T).(\lambda (H5: (pr0 (THead (Flat Cast) t3 t2) t4)).(let
-H6 \def (match H5 in pr0 return (\lambda (t5: T).(\lambda (t6: T).(\lambda
-(_: (pr0 t5 t6)).((eq T t5 (THead (Flat Cast) t3 t2)) \to ((eq T t6 t4) \to
-(ty3 g c2 t4 t3)))))) with [(pr0_refl t5) \Rightarrow (\lambda (H6: (eq T t5
-(THead (Flat Cast) t3 t2))).(\lambda (H7: (eq T t5 t4)).(eq_ind T (THead
-(Flat Cast) t3 t2) (\lambda (t6: T).((eq T t6 t4) \to (ty3 g c2 t4 t3)))
-(\lambda (H8: (eq T (THead (Flat Cast) t3 t2) t4)).(eq_ind T (THead (Flat
-Cast) t3 t2) (\lambda (t6: T).(ty3 g c2 t6 t3)) (ty3_cast g c2 t2 t3 (H1 c2
-H4 t2 (pr0_refl t2)) t0 (H3 c2 H4 t3 (pr0_refl t3))) t4 H8)) t5 (sym_eq T t5
-(THead (Flat Cast) t3 t2) H6) H7))) | (pr0_comp u1 u2 H6 t5 t6 H7 k)
-\Rightarrow (\lambda (H8: (eq T (THead k u1 t5) (THead (Flat Cast) t3
-t2))).(\lambda (H9: (eq T (THead k u2 t6) t4)).((let H10 \def (f_equal T T
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) \Rightarrow t7]))
-(THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H11 \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 t5) (THead (Flat Cast) t3 t2) H8) in ((let H12 \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 t5) (THead (Flat Cast) t3 t2) H8) in (eq_ind K (Flat Cast)
-(\lambda (k0: K).((eq T u1 t3) \to ((eq T t5 t2) \to ((eq T (THead k0 u2 t6)
-t4) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4 t3))))))) (\lambda
-(H13: (eq T u1 t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t5 t2) \to ((eq T
-(THead (Flat Cast) u2 t6) t4) \to ((pr0 t7 u2) \to ((pr0 t5 t6) \to (ty3 g c2
-t4 t3)))))) (\lambda (H14: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T
+False])])) I (THead (Flat Appl) w v) H9) in (False_ind ((eq T (THead (Bind
+Abbr) u2 w0) t2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to ((subst0 O u2 t4 w0)
+\to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))) H11))
+H10 H6 H7 H8))) | (pr0_zeta b H6 t3 t4 H7 u0) \Rightarrow (\lambda (H8: (eq T
+(THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Appl) w v))).(\lambda (H9:
+(eq T t4 t2)).((let H10 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O 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 True |
+(Flat _) \Rightarrow False])])) I (THead (Flat Appl) w v) H8) in (False_ind
+((eq T t4 t2) \to ((not (eq B b Abst)) \to ((pr0 t3 t4) \to (ty3 g c2 t2
+(THead (Flat Appl) w (THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) |
+(pr0_epsilon t3 t4 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast)
+u0 t3) (THead (Flat Appl) w v))).(\lambda (H8: (eq T t4 t2)).((let H9 \def
+(eq_ind T (THead (Flat Cast) u0 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 False | Cast
+\Rightarrow True])])])) I (THead (Flat Appl) w v) H7) in (False_ind ((eq T t4
+t2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst)
+u t0))))) H9)) H8 H6)))]) in (H6 (refl_equal T (THead (Flat Appl) w v))
+(refl_equal T t2)))))))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda
+(t3: T).(\lambda (_: (ty3 g c t2 t3)).(\lambda (H1: ((\forall (c2: C).((wcpr0
+c c2) \to (\forall (t4: T).((pr0 t2 t4) \to (ty3 g c2 t4 t3))))))).(\lambda
+(t0: T).(\lambda (_: (ty3 g c t3 t0)).(\lambda (H3: ((\forall (c2: C).((wcpr0
+c c2) \to (\forall (t4: T).((pr0 t3 t4) \to (ty3 g c2 t4 t0))))))).(\lambda
+(c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t4: T).(\lambda (H5: (pr0
+(THead (Flat Cast) t3 t2) t4)).(let H6 \def (match H5 in pr0 return (\lambda
+(t5: T).(\lambda (t6: T).(\lambda (_: (pr0 t5 t6)).((eq T t5 (THead (Flat
+Cast) t3 t2)) \to ((eq T t6 t4) \to (ty3 g c2 t4 (THead (Flat Cast) t0
+t3))))))) with [(pr0_refl t5) \Rightarrow (\lambda (H6: (eq T t5 (THead (Flat
+Cast) t3 t2))).(\lambda (H7: (eq T t5 t4)).(eq_ind T (THead (Flat Cast) t3
+t2) (\lambda (t6: T).((eq T t6 t4) \to (ty3 g c2 t4 (THead (Flat Cast) t0
+t3)))) (\lambda (H8: (eq T (THead (Flat Cast) t3 t2) t4)).(eq_ind T (THead
+(Flat Cast) t3 t2) (\lambda (t6: T).(ty3 g c2 t6 (THead (Flat Cast) t0 t3)))
+(ty3_cast g c2 t2 t3 (H1 c2 H4 t2 (pr0_refl t2)) t0 (H3 c2 H4 t3 (pr0_refl
+t3))) t4 H8)) t5 (sym_eq T t5 (THead (Flat Cast) t3 t2) H6) H7))) | (pr0_comp
+u1 u2 H6 t5 t6 H7 k) \Rightarrow (\lambda (H8: (eq T (THead k u1 t5) (THead
+(Flat Cast) t3 t2))).(\lambda (H9: (eq T (THead k u2 t6) t4)).((let H10 \def
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
+[(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7)
+\Rightarrow t7])) (THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H11
+\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 t5) (THead (Flat Cast) t3 t2) H8) in ((let H12
+\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 t5) (THead (Flat Cast) t3 t2) H8) in (eq_ind K
+(Flat Cast) (\lambda (k0: K).((eq T u1 t3) \to ((eq T t5 t2) \to ((eq T
+(THead k0 u2 t6) t4) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4
+(THead (Flat Cast) t0 t3)))))))) (\lambda (H13: (eq T u1 t3)).(eq_ind T t3
+(\lambda (t7: T).((eq T t5 t2) \to ((eq T (THead (Flat Cast) u2 t6) t4) \to
+((pr0 t7 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0
+t3))))))) (\lambda (H14: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T