-(_: 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 _)
+(_: 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 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) 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 with [(TSort _)