-(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
-False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2:
-T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O
-v) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (b0: B).(\lambda (c0:
-C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g
-(CHead c0 (Bind b0) v) t0 t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u
-t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind
-b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
-(H3: (eq T (THead (Bind b0) v t0) (THead (Bind b) u t1))).(let H4 \def
-(f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with
-[(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
-\Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v t0) (THead
-(Bind b) u t1) H3) in ((let H5 \def (f_equal T T (\lambda (e: T).(match e in
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _)
-\Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v t0) (THead
-(Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e: T).(match e in
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
-\Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead
-(Bind b) u t1) H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0
-b)).(let H9 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1))
-\to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u)
-t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in
-(let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t
-t2)) H1 t1 H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead
-(Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind
-b0) t) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u
-t3)))))) H9 u H7) in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead
-c0 (Bind b0) t) t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1)
+H4) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1
+t2)) (\lambda (t2: T).(eq T (lift (S i) O v) (THead (Bind b) u t2))))
+H5))))))))))) (\lambda (b0: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0:
+T).(\lambda (t2: T).(\lambda (H1: (sty0 g (CHead c0 (Bind b0) v) t0
+t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3:
+T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u) t1 t3)) (\lambda (t3:
+T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T (THead (Bind b0)
+v t0) (THead (Bind b) u t1))).(let H4 \def (f_equal T B (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 |
+(THead k _ _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat _)
+\Rightarrow b0])])) (THead (Bind b0) v t0) (THead (Bind b) u t1) H3) in ((let
+H5 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v |
+(TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v
+t0) (THead (Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
+(THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead (Bind b) u t1)
+H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0 b)).(let H9 \def
+(eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1)) \to (ex2 T
+(\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u) t1 t3))
+(\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in (let H10
+\def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t t2)) H1 t1
+H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead (Bind b) u
+t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) t) (Bind
+b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H9 u H7)
+in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) t)
+t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T (\lambda (t3:
+T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind
+b0) t t2) (THead (Bind b) u t3))))) (let H13 \def (eq_ind B b0 (\lambda (b1:
+B).((eq T t1 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g
+(CHead (CHead c0 (Bind b1) u) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2
+(THead (Bind b) u t3)))))) H11 b H8) in (let H14 \def (eq_ind B b0 (\lambda
+(b1: B).(sty0 g (CHead c0 (Bind b1) u) t1 t2)) H12 b H8) in (eq_ind_r B b
+(\lambda (b1: B).(ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1
+t3)) (\lambda (t3: T).(eq T (THead (Bind b1) u t2) (THead (Bind b) u t3)))))
+(ex_intro2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda
+(t3: T).(eq T (THead (Bind b) u t2) (THead (Bind b) u t3))) t2 H14
+(refl_equal T (THead (Bind b) u t2))) b0 H8))) v H7)))))))) H5)) H4))))))))))
+(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda
+(_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u t1)) \to
+(ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3:
+T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T (THead (Flat
+Appl) v t0) (THead (Bind b) u t1))).(let H4 \def (eq_ind T (THead (Flat Appl)
+v t0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef
+_) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t1)
+H3) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1
+t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Bind b) u t3))))
+H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
+(sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t1)) \to (ex2 T
+(\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T
+v2 (THead (Bind b) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_:
+(sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u t1)) \to (ex2 T