-(TLRef _) \Rightarrow t0 | (THead _ _ t4) \Rightarrow t4])) (THead (Bind b0)
-u0 t0) (THead (Bind b) u t1) H7) in (\lambda (H11: (eq T u0 u)).(\lambda
-(H12: (eq B b0 b)).(let H13 \def (eq_ind T t0 (\lambda (t4: T).((eq T t4
-(THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t5: T).(\lambda (_:
-T).(\lambda (_: T).(pc3 (CHead c0 (Bind b0) u0) (THead (Bind b) u t5) t2))))
-(\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b0)
-u0) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead
-(CHead c0 (Bind b0) u0) (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
-T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t5
-t7))))))) H4 t1 H10) in (let H14 \def (eq_ind T t0 (\lambda (t4: T).(ty3 g
-(CHead c0 (Bind b0) u0) t4 t2)) H3 t1 H10) in (let H15 \def (eq_ind B b0
-(\lambda (b1: B).((eq T t2 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda
-(t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b1) u0) (THead
-(Bind b) u t4) t3)))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g
-(CHead c0 (Bind b1) u0) u t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda
-(_: T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind b) u) t1 t4)))) (\lambda
-(t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead (CHead c0 (Bind b1)
-u0) (Bind b) u) t4 t6))))))) H6 b H12) in (let H16 \def (eq_ind B b0 (\lambda
-(b1: B).(ty3 g (CHead c0 (Bind b1) u0) t2 t3)) H5 b H12) in (let H17 \def
-(eq_ind B b0 (\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex4_3 T T
-T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b1)
-u0) (THead (Bind b) u t4) t2)))) (\lambda (_: T).(\lambda (t5: T).(\lambda
-(_: T).(ty3 g (CHead c0 (Bind b1) u0) u t5)))) (\lambda (t4: T).(\lambda (_:
-T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind b) u) t1
-t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead (CHead
-c0 (Bind b1) u0) (Bind b) u) t4 t6))))))) H13 b H12) in (let H18 \def (eq_ind
-B b0 (\lambda (b1: B).(ty3 g (CHead c0 (Bind b1) u0) t1 t2)) H14 b H12) in
-(eq_ind_r B b (\lambda (b1: B).(ex4_3 T T T (\lambda (t4: T).(\lambda (_:
-T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) (THead (Bind b1) u0 t2)))))
-(\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c0 u t5)))) (\lambda
-(t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
-t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c0
-(Bind b) u) t4 t6)))))) (let H19 \def (eq_ind T u0 (\lambda (t4: T).((eq T t2
-(THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t5: T).(\lambda (_:
-T).(\lambda (_: T).(pc3 (CHead c0 (Bind b) t4) (THead (Bind b) u t5) t3))))
-(\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b)
-t4) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead
-(CHead c0 (Bind b) t4) (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
-T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b) t4) (Bind b) u) t5
-t7))))))) H15 u H11) in (let H20 \def (eq_ind T u0 (\lambda (t4: T).(ty3 g
-(CHead c0 (Bind b) t4) t2 t3)) H16 u H11) in (let H21 \def (eq_ind T u0
-(\lambda (t4: T).((eq T t1 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda
-(t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b) t4) (THead
-(Bind b) u t5) t2)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g
-(CHead c0 (Bind b) t4) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
-T).(ty3 g (CHead (CHead c0 (Bind b) t4) (Bind b) u) t1 t5)))) (\lambda (t5:
-T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b) t4)
-(Bind b) u) t5 t7))))))) H17 u H11) in (let H22 \def (eq_ind T u0 (\lambda
-(t4: T).(ty3 g (CHead c0 (Bind b) t4) t1 t2)) H18 u H11) in (let H23 \def
-(eq_ind T u0 (\lambda (t4: T).((eq T t4 (THead (Bind b) u t1)) \to (ex4_3 T T
-T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
-t5) t)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c0 u t6))))
-(\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u)
-t1 t5)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c0
-(Bind b) u) t5 t7))))))) H2 u H11) in (let H24 \def (eq_ind T u0 (\lambda
-(t4: T).(ty3 g c0 t4 t)) H1 u H11) in (eq_ind_r T u (\lambda (t4: T).(ex4_3 T
-T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
-u t5) (THead (Bind b) t4 t2))))) (\lambda (_: T).(\lambda (t6: T).(\lambda
-(_: T).(ty3 g c0 u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
-T).(ty3 g (CHead c0 (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
-T).(\lambda (t7: T).(ty3 g (CHead c0 (Bind b) u) t5 t7)))))) (ex4_3_intro T T
-T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
-t4) (THead (Bind b) u t2))))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_:
-T).(ty3 g c0 u t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
-(CHead c0 (Bind b) u) t1 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda
-(t6: T).(ty3 g (CHead c0 (Bind b) u) t4 t6)))) t2 t t3 (pc3_refl c0 (THead
-(Bind b) u t2)) H24 H22 H20) u0 H11))))))) b0 H12)))))))))) H9))
-H8)))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda
-(_: (ty3 g c0 w u0)).(\lambda (_: (((eq T w (THead (Bind b) u t1)) \to (ex4_3
-T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind
-b) u t2) u0)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u
-t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind
-b) u) t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g
-(CHead c0 (Bind b) u) t2 t0)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda
-(_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (_: (((eq T v (THead
-(Bind b) u t1)) \to (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda
-(_: T).(pc3 c0 (THead (Bind b) u t2) (THead (Bind Abst) u0 t))))) (\lambda
-(_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t2:
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
-(\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b)
-u) t2 t3)))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (THead (Bind b)
-u t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w v) (\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 b) u t1) H5) in (False_ind (ex4_3 T T T
-(\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
-t2) (THead (Flat Appl) w (THead (Bind Abst) u0 t)))))) (\lambda (_:
-T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t2:
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
-(\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b)
-u) t2 t3))))) H6)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2:
-T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u
-t1)) \to (ex4_3 T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3
-c0 (THead (Bind b) u t3) t2)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_:
-T).(ty3 g c0 u t)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
-(CHead c0 (Bind b) u) t1 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda
-(t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))))))).(\lambda (t3: T).(\lambda
-(_: (ty3 g c0 t2 t3)).(\lambda (_: (((eq T t2 (THead (Bind b) u t1)) \to
-(ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead
-(Bind b) u t4) t3)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g
-c0 u t)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
-(Bind b) u) t1 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t5: T).(ty3
-g (CHead c0 (Bind b) u) t4 t5)))))))).(\lambda (H5: (eq T (THead (Flat Cast)
-t2 t0) (THead (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) t2
-t0) (\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 b) u t1)
-H5) in (False_ind (ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_:
-T).(pc3 c0 (THead (Bind b) u t4) (THead (Flat Cast) t3 t2))))) (\lambda (_:
-T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u t)))) (\lambda (t4:
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))
-(\lambda (t4: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b)
-u) t4 t5))))) H6))))))))))) c y x H0))) H))))))).
+(TLRef _) \Rightarrow t0 | (THead _ _ t3) \Rightarrow t3])) (THead (Bind b0)
+u0 t0) (THead (Bind b) u t1) H5) in (\lambda (H9: (eq T u0 u)).(\lambda (H10:
+(eq B b0 b)).(let H11 \def (eq_ind T t0 (\lambda (t3: T).((eq T t3 (THead
+(Bind b) u t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 (CHead
+c0 (Bind b0) u0) (THead (Bind b) u t4) t2))) (\lambda (_: T).(\lambda (t5:
+T).(ty3 g (CHead c0 (Bind b0) u0) u t5))) (\lambda (t4: T).(\lambda (_:
+T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t1 t4)))))) H4 t1 H8) in
+(let H12 \def (eq_ind T t0 (\lambda (t3: T).(ty3 g (CHead c0 (Bind b0) u0) t3
+t2)) H3 t1 H8) in (let H13 \def (eq_ind B b0 (\lambda (b1: B).((eq T t1
+(THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3
+(CHead c0 (Bind b1) u0) (THead (Bind b) u t3) t2))) (\lambda (_: T).(\lambda
+(t4: T).(ty3 g (CHead c0 (Bind b1) u0) u t4))) (\lambda (t3: T).(\lambda (_:
+T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind b) u) t1 t3)))))) H11 b H10)
+in (let H14 \def (eq_ind B b0 (\lambda (b1: B).(ty3 g (CHead c0 (Bind b1) u0)
+t1 t2)) H12 b H10) in (eq_ind_r B b (\lambda (b1: B).(ex3_2 T T (\lambda (t3:
+T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) (THead (Bind b1) u0 t2))))
+(\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u t4))) (\lambda (t3: T).(\lambda
+(_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))) (let H15 \def (eq_ind T u0
+(\lambda (t3: T).((eq T t1 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
+(t4: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b) t3) (THead (Bind b) u t4)
+t2))) (\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b) t3) u t5)))
+(\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b) t3) (Bind
+b) u) t1 t4)))))) H13 u H9) in (let H16 \def (eq_ind T u0 (\lambda (t3:
+T).(ty3 g (CHead c0 (Bind b) t3) t1 t2)) H14 u H9) in (let H17 \def (eq_ind T
+u0 (\lambda (t3: T).((eq T t3 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
+(t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) t))) (\lambda (_:
+T).(\lambda (t5: T).(ty3 g c0 u t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 g
+(CHead c0 (Bind b) u) t1 t4)))))) H2 u H9) in (let H18 \def (eq_ind T u0
+(\lambda (t3: T).(ty3 g c0 t3 t)) H1 u H9) in (eq_ind_r T u (\lambda (t3:
+T).(ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4)
+(THead (Bind b) t3 t2)))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u t5)))
+(\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4)))))
+(ex3_2_intro T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
+t3) (THead (Bind b) u t2)))) (\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u
+t4))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3)))
+t2 t (pc3_refl c0 (THead (Bind b) u t2)) H18 H16) u0 H9))))) b0 H10))))))))
+H7)) H6))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u0:
+T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (_: (((eq T w (THead (Bind b) u
+t1)) \to (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
+u t2) u0))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t2:
+T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))))).(\lambda (v:
+T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0
+t))).(\lambda (_: (((eq T v (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
+(t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t2) (THead (Bind Abst) u0
+t)))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u t0))) (\lambda (t2:
+T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))))).(\lambda (H5:
+(eq T (THead (Flat Appl) w v) (THead (Bind b) u t1))).(let H6 \def (eq_ind T
+(THead (Flat Appl) w v) (\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
+b) u t1) H5) in (False_ind (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3
+c0 (THead (Bind b) u t2) (THead (Flat Appl) w (THead (Bind Abst) u0 t)))))
+(\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u t0))) (\lambda (t2: T).(\lambda
+(_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2)))) H6)))))))))))) (\lambda (c0:
+C).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda
+(_: (((eq T t0 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t3:
+T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) t2))) (\lambda (_:
+T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t3: T).(\lambda (_: T).(ty3 g
+(CHead c0 (Bind b) u) t1 t3))))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2
+t3)).(\lambda (_: (((eq T t2 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
+(t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) t3))) (\lambda (_:
+T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t4: T).(\lambda (_: T).(ty3 g
+(CHead c0 (Bind b) u) t1 t4))))))).(\lambda (H5: (eq T (THead (Flat Cast) t2
+t0) (THead (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) t2 t0)
+(\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 b) u t1) H5) in (False_ind
+(ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4)
+(THead (Flat Cast) t3 t2)))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t)))
+(\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))
+H6))))))))))) c y x H0))) H))))))).