-c t5 t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq T t5 (THead
-(Flat Cast) x0 x1))).(\lambda (H9: (subst0 i u t3 x0)).(\lambda (H10: (subst0
-(s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda
-(t6: T).(ty3 g c t6 t3)) (ty3_conv g c t3 t0 H2 (THead (Flat Cast) x0 x1) x0
-(ty3_cast g c x1 x0 (ty3_conv g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c t3 x0
-H9) e H6) x1 t3 (H1 (s (Flat Cast) i) u c x1 (fsubst0_snd (s (Flat Cast) i) u
-c t2 x1 H10) e H6) (pc3_s c t3 x0 (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c
-x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t0 (H3 i u c x0 (fsubst0_snd i u c t3
-x0 H9) e H6)) (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x0 (fsubst0_snd i u
-c t3 x0 H9) e H6)) t5 H8)))))) H7)) (subst0_gen_head (Flat Cast) u t3 t2 t5 i
-H5)))))) (\lambda (c3: C).(\lambda (H5: (csubst0 i u c c3)).(\lambda (e:
-C).(\lambda (H6: (getl i c (CHead e (Bind Abbr) u))).(ty3_cast g c3 t2 t3 (H1
-i u c3 t2 (fsubst0_fst i u c t2 c3 H5) e H6) t0 (H3 i u c3 t3 (fsubst0_fst i
-u c t3 c3 H5) e H6)))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u (THead
-(Flat Cast) t3 t2) t5)).(\lambda (c3: C).(\lambda (H6: (csubst0 i u c
-c3)).(\lambda (e: C).(\lambda (H7: (getl i c (CHead e (Bind Abbr)
-u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2)))
-(\lambda (u2: T).(subst0 i u t3 u2))) (ex2 T (\lambda (t6: T).(eq T t5 (THead
-(Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)))
-(ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2
-t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_:
-T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)))) (ty3 g c3 t5 t3)
-(\lambda (H8: (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2)))
-(\lambda (u2: T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t5
-(THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)) (ty3 g c3 t5
-t3) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x
+c t5 (THead (Flat Cast) t0 t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda
+(H8: (eq T t5 (THead (Flat Cast) x0 x1))).(\lambda (H9: (subst0 i u t3
+x0)).(\lambda (H10: (subst0 (s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead
+(Flat Cast) x0 x1) (\lambda (t6: T).(ty3 g c t6 (THead (Flat Cast) t0 t3)))
+(ex_ind T (\lambda (t6: T).(ty3 g c t0 t6)) (ty3 g c (THead (Flat Cast) x0
+x1) (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H11: (ty3 g c t0
+x)).(ty3_conv g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0)
+(ty3_cast g c t3 t0 H2 x H11) (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0
+x0) (ty3_cast g c x1 x0 (ty3_conv g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c
+t3 x0 H9) e H6) x1 t3 (H1 (s (Flat Cast) i) u c x1 (fsubst0_snd (s (Flat
+Cast) i) u c t2 x1 H10) e H6) (pc3_s c t3 x0 (pc3_fsubst0 c t3 t3 (pc3_refl c
+t3) i u c x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t0 (H3 i u c x0
+(fsubst0_snd i u c t3 x0 H9) e H6)) (pc3_fsubst0 c (THead (Flat Cast) t0 t3)
+(THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat Cast) t0 t3)) i u c (THead
+(Flat Cast) t0 x0) (fsubst0_snd i u c (THead (Flat Cast) t0 t3) (THead (Flat
+Cast) t0 x0) (subst0_snd (Flat Cast) u x0 t3 i H9 t0)) e H6)))) (ty3_correct
+g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t5 H8)))))) H7))
+(subst0_gen_head (Flat Cast) u t3 t2 t5 i H5)))))) (\lambda (c3: C).(\lambda
+(H5: (csubst0 i u c c3)).(\lambda (e: C).(\lambda (H6: (getl i c (CHead e
+(Bind Abbr) u))).(ty3_cast g c3 t2 t3 (H1 i u c3 t2 (fsubst0_fst i u c t2 c3
+H5) e H6) t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H5) e H6)))))) (\lambda
+(t5: T).(\lambda (H5: (subst0 i u (THead (Flat Cast) t3 t2) t5)).(\lambda
+(c3: C).(\lambda (H6: (csubst0 i u c c3)).(\lambda (e: C).(\lambda (H7: (getl
+i c (CHead e (Bind Abbr) u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5
+(THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2))) (ex2 T
+(\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6:
+T).(subst0 (s (Flat Cast) i) u t2 t6))) (ex3_2 T T (\lambda (u2: T).(\lambda
+(t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: T).(\lambda (_:
+T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Flat
+Cast) i) u t2 t6)))) (ty3 g c3 t5 (THead (Flat Cast) t0 t3)) (\lambda (H8:
+(ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2))) (\lambda (u2:
+T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t5 (THead (Flat
+Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)) (ty3 g c3 t5 (THead (Flat
+Cast) t0 t3)) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x