-(THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (land (pc3 c t2 x)
-(ty3 g c t1 t2)) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(ty3_ind g
-(\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Flat Cast)
-t2 t1)) \to (land (pc3 c0 t2 t0) (ty3 g c0 t1 t2)))))) (\lambda (c0:
-C).(\lambda (t0: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t0 t)).(\lambda
-(_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 t) (ty3 g c0
-t1 t2))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u
-t3)).(\lambda (H4: (((eq T u (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2
-t3) (ty3 g c0 t1 t2))))).(\lambda (H5: (pc3 c0 t3 t0)).(\lambda (H6: (eq T u
-(THead (Flat Cast) t2 t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u
-(THead (Flat Cast) t2 t1) H6) in (let H8 \def (eq_ind T u (\lambda (t4:
-T).((eq T t4 (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 t3) (ty3 g c0 t1
-t2)))) H4 (THead (Flat Cast) t2 t1) H7) in (let H9 \def (eq_ind T u (\lambda
-(t4: T).(ty3 g c0 t4 t3)) H3 (THead (Flat Cast) t2 t1) H7) in (let H10 \def
-(H8 (refl_equal T (THead (Flat Cast) t2 t1))) in (and_ind (pc3 c0 t2 t3) (ty3
-g c0 t1 t2) (land (pc3 c0 t2 t0) (ty3 g c0 t1 t2)) (\lambda (H11: (pc3 c0 t2
-t3)).(\lambda (H12: (ty3 g c0 t1 t2)).(conj (pc3 c0 t2 t0) (ty3 g c0 t1 t2)
-(pc3_t t3 c0 t2 H11 t0 H5) H12))) H10)))))))))))))))) (\lambda (c0:
-C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (THead (Flat Cast) t2
-t1))).(let H2 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast)
-t2 t1) H1) in (False_ind (land (pc3 c0 t2 (TSort (next g m))) (ty3 g c0 t1
-t2)) H2))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u:
-T).(\lambda (_: (getl n c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda
-(_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to
-(land (pc3 d t2 t) (ty3 g d t1 t2))))).(\lambda (H4: (eq T (TLRef n) (THead
+(THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (ex3 T (\lambda (t0:
+T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2))
+(\lambda (t0: T).(ty3 g c t2 t0))) (\lambda (y: T).(\lambda (H0: (ty3 g c y
+x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t
+(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat
+Cast) t3 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g
+c0 t2 t3))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t: T).(\lambda
+(_: (ty3 g c0 t0 t)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to
+(ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat Cast) t3 t2) t)) (\lambda (_:
+T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g c0 t2 t3)))))).(\lambda (u:
+T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u t3)).(\lambda (H4: (((eq T u
+(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat
+Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g
+c0 t2 t4)))))).(\lambda (H5: (pc3 c0 t3 t0)).(\lambda (H6: (eq T u (THead
+(Flat Cast) t2 t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u (THead
+(Flat Cast) t2 t1) H6) in (let H8 \def (eq_ind T u (\lambda (t4: T).((eq T t4
+(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat
+Cast) t5 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g
+c0 t2 t5))))) H4 (THead (Flat Cast) t2 t1) H7) in (let H9 \def (eq_ind T u
+(\lambda (t4: T).(ty3 g c0 t4 t3)) H3 (THead (Flat Cast) t2 t1) H7) in (let
+H10 \def (H8 (refl_equal T (THead (Flat Cast) t2 t1))) in (ex3_ind T (\lambda
+(t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1
+t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) (ex3 T (\lambda (t4: T).(pc3 c0
+(THead (Flat Cast) t4 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda
+(t4: T).(ty3 g c0 t2 t4))) (\lambda (x0: T).(\lambda (H11: (pc3 c0 (THead
+(Flat Cast) x0 t2) t3)).(\lambda (H12: (ty3 g c0 t1 t2)).(\lambda (H13: (ty3
+g c0 t2 x0)).(ex3_intro T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2)
+t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) x0
+(pc3_t t3 c0 (THead (Flat Cast) x0 t2) H11 t0 H5) H12 H13)))))
+H10)))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T
+(TSort m) (THead (Flat Cast) t2 t1))).(let H2 \def (eq_ind T (TSort m)
+(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+False])) I (THead (Flat Cast) t2 t1) H1) in (False_ind (ex3 T (\lambda (t0:
+T).(pc3 c0 (THead (Flat Cast) t0 t2) (TSort (next g m)))) (\lambda (_:
+T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H2))))) (\lambda (n:
+nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0
+(CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u
+t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda
+(t0: T).(pc3 d (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2))
+(\lambda (t0: T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead