X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Ffsubst0.ma;h=7a71c7d359c61ba3ed3a97eb3f389e35aa6d9ee8;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=4bc299e430afce87d6c4ec55d297b69229a02cc1;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma
index 4bc299e43..7a71c7d35 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma
@@ -14,15 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0".
+include "LambdaDelta-1/ty3/props.ma".
 
-include "ty3/props.ma".
+include "LambdaDelta-1/pc3/fsubst0.ma".
 
-include "pc3/fsubst0.ma".
+include "LambdaDelta-1/csubst0/props.ma".
 
-include "csubst0/props.ma".
-
-include "getl/getl.ma".
+include "LambdaDelta-1/getl/getl.ma".
 
 theorem ty3_fsubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1 
@@ -80,7 +78,7 @@ t0)))))))))).(\lambda (i: nat).(\lambda (u0: T).(\lambda (c2: C).(\lambda
 (TLRef n) (\lambda (c0: C).(\lambda (t3: T).(\forall (e: C).((getl i c (CHead 
 e (Bind Abbr) u0)) \to (ty3 g c0 t3 (lift (S n) O t0)))))) (\lambda (t3: 
 T).(\lambda (H4: (subst0 i u0 (TLRef n) t3)).(\lambda (e: C).(\lambda (H5: 
-(getl i c (CHead e (Bind Abbr) u0))).(and_ind (eq nat n i) (eq T t3 (lift (S 
+(getl i c (CHead e (Bind Abbr) u0))).(land_ind (eq nat n i) (eq T t3 (lift (S 
 n) O u0)) (ty3 g c t3 (lift (S n) O t0)) (\lambda (H6: (eq nat n i)).(\lambda 
 (H7: (eq T t3 (lift (S n) O u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4: 
 T).(ty3 g c t4 (lift (S n) O t0))) (let H8 \def (eq_ind_r nat i (\lambda (n0: 
@@ -239,7 +237,7 @@ H14)) H13))))))))))) H8)) H7))) (\lambda (H6: (le i n)).(ty3_abbr g n c3 d u
 (csubst0_getl_ge i n H6 c c3 u0 H4 (CHead d (Bind Abbr) u) H0) t0 H1))))))) 
 (\lambda (t3: T).(\lambda (H4: (subst0 i u0 (TLRef n) t3)).(\lambda (c3: 
 C).(\lambda (H5: (csubst0 i u0 c c3)).(\lambda (e: C).(\lambda (H6: (getl i c 
-(CHead e (Bind Abbr) u0))).(and_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) 
+(CHead e (Bind Abbr) u0))).(land_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) 
 (ty3 g c3 t3 (lift (S n) O t0)) (\lambda (H7: (eq nat n i)).(\lambda (H8: (eq 
 T t3 (lift (S n) O u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4: T).(ty3 
 g c3 t4 (lift (S n) O t0))) (let H9 \def (eq_ind_r nat i (\lambda (n0: 
@@ -273,7 +271,7 @@ c2 t2)).(fsubst0_ind i u0 c (TLRef n) (\lambda (c0: C).(\lambda (t3:
 T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u0)) \to (ty3 g c0 t3 
 (lift (S n) O u)))))) (\lambda (t3: T).(\lambda (H4: (subst0 i u0 (TLRef n) 
 t3)).(\lambda (e: C).(\lambda (H5: (getl i c (CHead e (Bind Abbr) 
-u0))).(and_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) (ty3 g c t3 (lift (S 
+u0))).(land_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) (ty3 g c t3 (lift (S 
 n) O u)) (\lambda (H6: (eq nat n i)).(\lambda (H7: (eq T t3 (lift (S n) O 
 u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4: T).(ty3 g c t4 (lift (S n) 
 O u))) (let H8 \def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c (CHead e 
@@ -442,8 +440,8 @@ H7))) (\lambda (H6: (le i n)).(ty3_abst g n c3 d u (csubst0_getl_ge i n H6 c
 c3 u0 H4 (CHead d (Bind Abst) u) H0) t0 H1))))))) (\lambda (t3: T).(\lambda 
 (H4: (subst0 i u0 (TLRef n) t3)).(\lambda (c3: C).(\lambda (H5: (csubst0 i u0 
 c c3)).(\lambda (e: C).(\lambda (H6: (getl i c (CHead e (Bind Abbr) 
-u0))).(and_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) (ty3 g c3 t3 (lift (S 
-n) O u)) (\lambda (H7: (eq nat n i)).(\lambda (H8: (eq T t3 (lift (S n) O 
+u0))).(land_ind (eq nat n i) (eq T t3 (lift (S n) O u0)) (ty3 g c3 t3 (lift 
+(S n) O u)) (\lambda (H7: (eq nat n i)).(\lambda (H8: (eq T t3 (lift (S n) O 
 u0))).(eq_ind_r T (lift (S n) O u0) (\lambda (t4: T).(ty3 g c3 t4 (lift (S n) 
 O u))) (let H9 \def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c (CHead e 
 (Bind Abbr) u0))) H6 n H7) in (let H10 \def (eq_ind_r nat i (\lambda (n0: 
@@ -462,195 +460,189 @@ H4)))))))) c2 t2 H3)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda
 (t0: T).(\lambda (H0: (ty3 g c u t0)).(\lambda (H1: ((\forall (i: 
 nat).(\forall (u0: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u0 c u c2 
 t2) \to (\forall (e: C).((getl i c (CHead e (Bind Abbr) u0)) \to (ty3 g c2 t2 
-t0)))))))))).(\lambda (b: B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: 
+t0)))))))))).(\lambda (b: B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2: 
 (ty3 g (CHead c (Bind b) u) t2 t3)).(\lambda (H3: ((\forall (i: nat).(\forall 
 (u0: T).(\forall (c2: C).(\forall (t4: T).((fsubst0 i u0 (CHead c (Bind b) u) 
 t2 c2 t4) \to (\forall (e: C).((getl i (CHead c (Bind b) u) (CHead e (Bind 
-Abbr) u0)) \to (ty3 g c2 t4 t3)))))))))).(\lambda (t4: T).(\lambda (H4: (ty3 
-g (CHead c (Bind b) u) t3 t4)).(\lambda (_: ((\forall (i: nat).(\forall (u0: 
-T).(\forall (c2: C).(\forall (t5: T).((fsubst0 i u0 (CHead c (Bind b) u) t3 
-c2 t5) \to (\forall (e: C).((getl i (CHead c (Bind b) u) (CHead e (Bind Abbr) 
-u0)) \to (ty3 g c2 t5 t4)))))))))).(\lambda (i: nat).(\lambda (u0: 
-T).(\lambda (c2: C).(\lambda (t5: T).(\lambda (H6: (fsubst0 i u0 c (THead 
-(Bind b) u t2) c2 t5)).(fsubst0_ind i u0 c (THead (Bind b) u t2) (\lambda 
-(c0: C).(\lambda (t6: T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u0)) 
-\to (ty3 g c0 t6 (THead (Bind b) u t3)))))) (\lambda (t6: T).(\lambda (H7: 
-(subst0 i u0 (THead (Bind b) u t2) t6)).(\lambda (e: C).(\lambda (H8: (getl i 
-c (CHead e (Bind Abbr) u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t6 (THead 
-(Bind b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t7: 
-T).(eq T t6 (THead (Bind b) u t7))) (\lambda (t7: T).(subst0 (s (Bind b) i) 
-u0 t2 t7))) (ex3_2 T T (\lambda (u2: T).(\lambda (t7: T).(eq T t6 (THead 
-(Bind b) u2 t7)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) 
-(\lambda (_: T).(\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7)))) (ty3 g c 
-t6 (THead (Bind b) u t3)) (\lambda (H9: (ex2 T (\lambda (u2: T).(eq T t6 
+Abbr) u0)) \to (ty3 g c2 t4 t3)))))))))).(\lambda (i: nat).(\lambda (u0: 
+T).(\lambda (c2: C).(\lambda (t4: T).(\lambda (H4: (fsubst0 i u0 c (THead 
+(Bind b) u t2) c2 t4)).(fsubst0_ind i u0 c (THead (Bind b) u t2) (\lambda 
+(c0: C).(\lambda (t5: T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u0)) 
+\to (ty3 g c0 t5 (THead (Bind b) u t3)))))) (\lambda (t5: T).(\lambda (H5: 
+(subst0 i u0 (THead (Bind b) u t2) t5)).(\lambda (e: C).(\lambda (H6: (getl i 
+c (CHead e (Bind Abbr) u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead 
+(Bind b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t6: 
+T).(eq T t5 (THead (Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) 
+u0 t2 t6))) (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) 
+(\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6)))) (ty3 g c 
+t5 (THead (Bind b) u t3)) (\lambda (H7: (ex2 T (\lambda (u2: T).(eq T t5 
 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2)))).(ex2_ind T 
-(\lambda (u2: T).(eq T t6 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i 
-u0 u u2)) (ty3 g c t6 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H10: 
-(eq T t6 (THead (Bind b) x t2))).(\lambda (H11: (subst0 i u0 u x)).(eq_ind_r 
-T (THead (Bind b) x t2) (\lambda (t7: T).(ty3 g c t7 (THead (Bind b) u t3))) 
-(ex_ind T (\lambda (t7: T).(ty3 g (CHead c (Bind b) u) t4 t7)) (ty3 g c 
-(THead (Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H12: 
-(ty3 g (CHead c (Bind b) u) t4 x0)).(ex_ind T (\lambda (t7: T).(ty3 g (CHead 
-c (Bind b) x) t3 t7)) (ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)) 
-(\lambda (x1: T).(\lambda (H13: (ty3 g (CHead c (Bind b) x) t3 x1)).(ty3_conv 
-g c (THead (Bind b) u t3) (THead (Bind b) u t4) (ty3_bind g c u t0 H0 b t3 t4 
-H4 x0 H12) (THead (Bind b) x t2) (THead (Bind b) x t3) (ty3_bind g c x t0 (H1 
-i u0 c x (fsubst0_snd i u0 c u x H11) e H8) b t2 t3 (H3 (S i) u0 (CHead c 
-(Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind 
-b) x) (csubst0_snd_bind b i u0 u x H11 c)) e (getl_head (Bind b) i c (CHead e 
-(Bind Abbr) u0) H8 u)) x1 H13) (pc3_fsubst0 c (THead (Bind b) u t3) (THead 
-(Bind b) u t3) (pc3_refl c (THead (Bind b) u t3)) i u0 c (THead (Bind b) x 
-t3) (fsubst0_snd i u0 c (THead (Bind b) u t3) (THead (Bind b) x t3) 
-(subst0_fst u0 x u i H11 t3 (Bind b))) e H8)))) (ty3_correct g (CHead c (Bind 
-b) x) t2 t3 (H3 (S i) u0 (CHead c (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead 
-c (Bind b) u) t2 (CHead c (Bind b) x) (csubst0_snd_bind b i u0 u x H11 c)) e 
-(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)))))) (ty3_correct g 
-(CHead c (Bind b) u) t3 t4 H4)) t6 H10)))) H9)) (\lambda (H9: (ex2 T (\lambda 
-(t7: T).(eq T t6 (THead (Bind b) u t7))) (\lambda (t7: T).(subst0 (s (Bind b) 
-i) u0 t2 t7)))).(ex2_ind T (\lambda (t7: T).(eq T t6 (THead (Bind b) u t7))) 
-(\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7)) (ty3 g c t6 (THead (Bind 
-b) u t3)) (\lambda (x: T).(\lambda (H10: (eq T t6 (THead (Bind b) u 
-x))).(\lambda (H11: (subst0 (s (Bind b) i) u0 t2 x)).(eq_ind_r T (THead (Bind 
-b) u x) (\lambda (t7: T).(ty3 g c t7 (THead (Bind b) u t3))) (ex_ind T 
-(\lambda (t7: T).(ty3 g (CHead c (Bind b) u) t3 t7)) (ty3 g c (THead (Bind b) 
-u x) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H12: (ty3 g (CHead c 
-(Bind b) u) t3 x0)).(ty3_bind g c u t0 H0 b x t3 (H3 (S i) u0 (CHead c (Bind 
-b) u) x (fsubst0_snd (S i) u0 (CHead c (Bind b) u) t2 x H11) e (getl_head 
-(Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x0 H12))) (ty3_correct g (CHead 
-c (Bind b) u) x t3 (H3 (S i) u0 (CHead c (Bind b) u) x (fsubst0_snd (S i) u0 
-(CHead c (Bind b) u) t2 x H11) e (getl_head (Bind b) i c (CHead e (Bind Abbr) 
-u0) H8 u)))) t6 H10)))) H9)) (\lambda (H9: (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7: 
-T).(subst0 (s (Bind b) i) u0 t2 t7))))).(ex3_2_ind T T (\lambda (u2: 
-T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7: 
-T).(subst0 (s (Bind b) i) u0 t2 t7))) (ty3 g c t6 (THead (Bind b) u t3)) 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (H10: (eq T t6 (THead (Bind b) x0 
-x1))).(\lambda (H11: (subst0 i u0 u x0)).(\lambda (H12: (subst0 (s (Bind b) 
-i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t7: T).(ty3 g c t7 
-(THead (Bind b) u t3))) (ex_ind T (\lambda (t7: T).(ty3 g (CHead c (Bind b) 
-u) t4 t7)) (ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)) (\lambda 
-(x: T).(\lambda (H13: (ty3 g (CHead c (Bind b) u) t4 x)).(ex_ind T (\lambda 
-(t7: T).(ty3 g (CHead c (Bind b) x0) t3 t7)) (ty3 g c (THead (Bind b) x0 x1) 
-(THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (H14: (ty3 g (CHead c (Bind 
-b) x0) t3 x2)).(ty3_conv g c (THead (Bind b) u t3) (THead (Bind b) u t4) 
-(ty3_bind g c u t0 H0 b t3 t4 H4 x H13) (THead (Bind b) x0 x1) (THead (Bind 
-b) x0 t3) (ty3_bind g c x0 t0 (H1 i u0 c x0 (fsubst0_snd i u0 c u x0 H11) e 
-H8) b x1 t3 (H3 (S i) u0 (CHead c (Bind b) x0) x1 (fsubst0_both (S i) u0 
-(CHead c (Bind b) u) t2 x1 H12 (CHead c (Bind b) x0) (csubst0_snd_bind b i u0 
-u x0 H11 c)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x2 
-H14) (pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c 
-(THead (Bind b) u t3)) i u0 c (THead (Bind b) x0 t3) (fsubst0_snd i u0 c 
-(THead (Bind b) u t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H11 t3 
-(Bind b))) e H8)))) (ty3_correct g (CHead c (Bind b) x0) x1 t3 (H3 (S i) u0 
-(CHead c (Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 
-H12 (CHead c (Bind b) x0) (csubst0_snd_bind b i u0 u x0 H11 c)) e (getl_head 
-(Bind b) i c (CHead e (Bind Abbr) u0) H8 u)))))) (ty3_correct g (CHead c 
-(Bind b) u) t3 t4 H4)) t6 H10)))))) H9)) (subst0_gen_head (Bind b) u0 u t2 t6 
-i H7)))))) (\lambda (c3: C).(\lambda (H7: (csubst0 i u0 c c3)).(\lambda (e: 
-C).(\lambda (H8: (getl i c (CHead e (Bind Abbr) u0))).(ex_ind T (\lambda (t6: 
-T).(ty3 g (CHead c3 (Bind b) u) t3 t6)) (ty3 g c3 (THead (Bind b) u t2) 
-(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H9: (ty3 g (CHead c3 (Bind 
-b) u) t3 x)).(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H7) e 
-H8) b t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 
-(CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 
-H7 u)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x H9))) 
-(ty3_correct g (CHead c3 (Bind b) u) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) 
-t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) 
-(csubst0_fst_bind b i c c3 u0 H7 u)) e (getl_head (Bind b) i c (CHead e (Bind 
-Abbr) u0) H8 u)))))))) (\lambda (t6: T).(\lambda (H7: (subst0 i u0 (THead 
-(Bind b) u t2) t6)).(\lambda (c3: C).(\lambda (H8: (csubst0 i u0 c 
-c3)).(\lambda (e: C).(\lambda (H9: (getl i c (CHead e (Bind Abbr) 
-u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t6 (THead (Bind b) u2 t2))) 
-(\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t7: T).(eq T t6 (THead 
-(Bind b) u t7))) (\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7))) (ex3_2 T 
-T (\lambda (u2: T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) 
+(\lambda (u2: T).(eq T t5 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i 
+u0 u u2)) (ty3 g c t5 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H8: 
+(eq T t5 (THead (Bind b) x t2))).(\lambda (H9: (subst0 i u0 u x)).(eq_ind_r T 
+(THead (Bind b) x t2) (\lambda (t6: T).(ty3 g c t6 (THead (Bind b) u t3))) 
+(ex_ind T (\lambda (t6: T).(ty3 g (CHead c (Bind b) u) t3 t6)) (ty3 g c 
+(THead (Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H10: 
+(ty3 g (CHead c (Bind b) u) t3 x0)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead 
+c (Bind b) x) t3 t6)) (ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3)) 
+(\lambda (x1: T).(\lambda (_: (ty3 g (CHead c (Bind b) x) t3 x1)).(ty3_conv g 
+c (THead (Bind b) u t3) (THead (Bind b) u x0) (ty3_bind g c u t0 H0 b t3 x0 
+H10) (THead (Bind b) x t2) (THead (Bind b) x t3) (ty3_bind g c x t0 (H1 i u0 
+c x (fsubst0_snd i u0 c u x H9) e H6) b t2 t3 (H3 (S i) u0 (CHead c (Bind b) 
+x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x) 
+(csubst0_snd_bind b i u0 u x H9 c)) e (getl_head (Bind b) i c (CHead e (Bind 
+Abbr) u0) H6 u))) (pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) 
+(pc3_refl c (THead (Bind b) u t3)) i u0 c (THead (Bind b) x t3) (fsubst0_snd 
+i u0 c (THead (Bind b) u t3) (THead (Bind b) x t3) (subst0_fst u0 x u i H9 t3 
+(Bind b))) e H6)))) (ty3_correct g (CHead c (Bind b) x) t2 t3 (H3 (S i) u0 
+(CHead c (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead 
+c (Bind b) x) (csubst0_snd_bind b i u0 u x H9 c)) e (getl_head (Bind b) i c 
+(CHead e (Bind Abbr) u0) H6 u)))))) (ty3_correct g (CHead c (Bind b) u) t2 t3 
+H2)) t5 H8)))) H7)) (\lambda (H7: (ex2 T (\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 
+t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Bind b) u t6))) (\lambda 
+(t6: T).(subst0 (s (Bind b) i) u0 t2 t6)) (ty3 g c t5 (THead (Bind b) u t3)) 
+(\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Bind b) u x))).(\lambda (H9: 
+(subst0 (s (Bind b) i) u0 t2 x)).(eq_ind_r T (THead (Bind b) u x) (\lambda 
+(t6: T).(ty3 g c t6 (THead (Bind b) u t3))) (ex_ind T (\lambda (t6: T).(ty3 g 
+(CHead c (Bind b) u) t3 t6)) (ty3 g c (THead (Bind b) u x) (THead (Bind b) u 
+t3)) (\lambda (x0: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 
+x0)).(ty3_bind g c u t0 H0 b x t3 (H3 (S i) u0 (CHead c (Bind b) u) x 
+(fsubst0_snd (S i) u0 (CHead c (Bind b) u) t2 x H9) e (getl_head (Bind b) i c 
+(CHead e (Bind Abbr) u0) H6 u))))) (ty3_correct g (CHead c (Bind b) u) x t3 
+(H3 (S i) u0 (CHead c (Bind b) u) x (fsubst0_snd (S i) u0 (CHead c (Bind b) 
+u) t2 x H9) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u)))) t5 
+H8)))) H7)) (\lambda (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T 
+t5 (THead (Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u 
+u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 
+t6))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) 
+(\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6))) (ty3 g c 
+t5 (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq 
+T t5 (THead (Bind b) x0 x1))).(\lambda (H9: (subst0 i u0 u x0)).(\lambda 
+(H10: (subst0 (s (Bind b) i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1) 
+(\lambda (t6: T).(ty3 g c t6 (THead (Bind b) u t3))) (ex_ind T (\lambda (t6: 
+T).(ty3 g (CHead c (Bind b) u) t3 t6)) (ty3 g c (THead (Bind b) x0 x1) (THead 
+(Bind b) u t3)) (\lambda (x: T).(\lambda (H11: (ty3 g (CHead c (Bind b) u) t3 
+x)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead c (Bind b) x0) t3 t6)) (ty3 g c 
+(THead (Bind b) x0 x1) (THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (_: 
+(ty3 g (CHead c (Bind b) x0) t3 x2)).(ty3_conv g c (THead (Bind b) u t3) 
+(THead (Bind b) u x) (ty3_bind g c u t0 H0 b t3 x H11) (THead (Bind b) x0 x1) 
+(THead (Bind b) x0 t3) (ty3_bind g c x0 t0 (H1 i u0 c x0 (fsubst0_snd i u0 c 
+u x0 H9) e H6) b x1 t3 (H3 (S i) u0 (CHead c (Bind b) x0) x1 (fsubst0_both (S 
+i) u0 (CHead c (Bind b) u) t2 x1 H10 (CHead c (Bind b) x0) (csubst0_snd_bind 
+b i u0 u x0 H9 c)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u))) 
+(pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c (THead 
+(Bind b) u t3)) i u0 c (THead (Bind b) x0 t3) (fsubst0_snd i u0 c (THead 
+(Bind b) u t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H9 t3 (Bind b))) 
+e H6)))) (ty3_correct g (CHead c (Bind b) x0) x1 t3 (H3 (S i) u0 (CHead c 
+(Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 H10 (CHead 
+c (Bind b) x0) (csubst0_snd_bind b i u0 u x0 H9 c)) e (getl_head (Bind b) i c 
+(CHead e (Bind Abbr) u0) H6 u)))))) (ty3_correct g (CHead c (Bind b) u) t2 t3 
+H2)) t5 H8)))))) H7)) (subst0_gen_head (Bind b) u0 u t2 t5 i H5)))))) 
+(\lambda (c3: C).(\lambda (H5: (csubst0 i u0 c c3)).(\lambda (e: C).(\lambda 
+(H6: (getl i c (CHead e (Bind Abbr) u0))).(ex_ind T (\lambda (t5: T).(ty3 g 
+(CHead c3 (Bind b) u) t3 t5)) (ty3 g c3 (THead (Bind b) u t2) (THead (Bind b) 
+u t3)) (\lambda (x: T).(\lambda (_: (ty3 g (CHead c3 (Bind b) u) t3 
+x)).(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H5) e H6) b t2 
+t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 (CHead c (Bind 
+b) u) t2 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 H5 u)) e 
+(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u))))) (ty3_correct g 
+(CHead c3 (Bind b) u) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 
+(fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) 
+(csubst0_fst_bind b i c c3 u0 H5 u)) e (getl_head (Bind b) i c (CHead e (Bind 
+Abbr) u0) H6 u)))))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u0 (THead 
+(Bind b) u t2) t5)).(\lambda (c3: C).(\lambda (H6: (csubst0 i u0 c 
+c3)).(\lambda (e: C).(\lambda (H7: (getl i c (CHead e (Bind Abbr) 
+u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Bind b) u2 t2))) 
+(\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6))) (ex3_2 T 
+T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Bind b) u2 t6)))) 
 (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: 
-T).(\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7)))) (ty3 g c3 t6 (THead 
-(Bind b) u t3)) (\lambda (H10: (ex2 T (\lambda (u2: T).(eq T t6 (THead (Bind 
+T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6)))) (ty3 g c3 t5 (THead 
+(Bind b) u t3)) (\lambda (H8: (ex2 T (\lambda (u2: T).(eq T t5 (THead (Bind 
 b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2)))).(ex2_ind T (\lambda (u2: 
-T).(eq T t6 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2)) 
-(ty3 g c3 t6 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H11: (eq T t6 
-(THead (Bind b) x t2))).(\lambda (H12: (subst0 i u0 u x)).(eq_ind_r T (THead 
-(Bind b) x t2) (\lambda (t7: T).(ty3 g c3 t7 (THead (Bind b) u t3))) (ex_ind 
-T (\lambda (t7: T).(ty3 g (CHead c3 (Bind b) u) t3 t7)) (ty3 g c3 (THead 
-(Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H13: (ty3 g 
-(CHead c3 (Bind b) u) t3 x0)).(ex_ind T (\lambda (t7: T).(ty3 g (CHead c3 
-(Bind b) u) x0 t7)) (ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)) 
-(\lambda (x1: T).(\lambda (H14: (ty3 g (CHead c3 (Bind b) u) x0 x1)).(ex_ind 
-T (\lambda (t7: T).(ty3 g (CHead c3 (Bind b) x) t3 t7)) (ty3 g c3 (THead 
-(Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (H15: (ty3 g 
-(CHead c3 (Bind b) x) t3 x2)).(ty3_conv g c3 (THead (Bind b) u t3) (THead 
-(Bind b) u x0) (ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H8) 
-e H9) b t3 x0 H13 x1 H14) (THead (Bind b) x t2) (THead (Bind b) x t3) 
-(ty3_bind g c3 x t0 (H1 i u0 c3 x (fsubst0_both i u0 c u x H12 c3 H8) e H9) b 
-t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c 
-(Bind b) u) t2 (CHead c3 (Bind b) x) (csubst0_both_bind b i u0 u x H12 c c3 
-H8)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H9 u)) x2 H15) 
-(pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c (THead 
-(Bind b) u t3)) i u0 c3 (THead (Bind b) x t3) (fsubst0_both i u0 c (THead 
-(Bind b) u t3) (THead (Bind b) x t3) (subst0_fst u0 x u i H12 t3 (Bind b)) c3 
-H8) e H9)))) (ty3_correct g (CHead c3 (Bind b) x) t2 t3 (H3 (S i) u0 (CHead 
+T).(eq T t5 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i u0 u u2)) 
+(ty3 g c3 t5 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H9: (eq T t5 
+(THead (Bind b) x t2))).(\lambda (H10: (subst0 i u0 u x)).(eq_ind_r T (THead 
+(Bind b) x t2) (\lambda (t6: T).(ty3 g c3 t6 (THead (Bind b) u t3))) (ex_ind 
+T (\lambda (t6: T).(ty3 g (CHead c3 (Bind b) u) t3 t6)) (ty3 g c3 (THead 
+(Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H11: (ty3 g 
+(CHead c3 (Bind b) u) t3 x0)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead c3 
+(Bind b) u) x0 t6)) (ty3 g c3 (THead (Bind b) x t2) (THead (Bind b) u t3)) 
+(\lambda (x1: T).(\lambda (_: (ty3 g (CHead c3 (Bind b) u) x0 x1)).(ex_ind T 
+(\lambda (t6: T).(ty3 g (CHead c3 (Bind b) x) t3 t6)) (ty3 g c3 (THead (Bind 
+b) x t2) (THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (_: (ty3 g (CHead 
+c3 (Bind b) x) t3 x2)).(ty3_conv g c3 (THead (Bind b) u t3) (THead (Bind b) u 
+x0) (ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H6) e H7) b t3 
+x0 H11) (THead (Bind b) x t2) (THead (Bind b) x t3) (ty3_bind g c3 x t0 (H1 i 
+u0 c3 x (fsubst0_both i u0 c u x H10 c3 H6) e H7) b t2 t3 (H3 (S i) u0 (CHead 
 c3 (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 
-(Bind b) x) (csubst0_both_bind b i u0 u x H12 c c3 H8)) e (getl_head (Bind b) 
-i c (CHead e (Bind Abbr) u0) H9 u)))))) (ty3_correct g (CHead c3 (Bind b) u) 
-t3 x0 H13)))) (ty3_correct g (CHead c3 (Bind b) u) t2 t3 (H3 (S i) u0 (CHead 
-c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 
-(Bind b) u) (csubst0_fst_bind b i c c3 u0 H8 u)) e (getl_head (Bind b) i c 
-(CHead e (Bind Abbr) u0) H9 u)))) t6 H11)))) H10)) (\lambda (H10: (ex2 T 
-(\lambda (t7: T).(eq T t6 (THead (Bind b) u t7))) (\lambda (t7: T).(subst0 (s 
-(Bind b) i) u0 t2 t7)))).(ex2_ind T (\lambda (t7: T).(eq T t6 (THead (Bind b) 
-u t7))) (\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7)) (ty3 g c3 t6 
-(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H11: (eq T t6 (THead (Bind 
-b) u x))).(\lambda (H12: (subst0 (s (Bind b) i) u0 t2 x)).(eq_ind_r T (THead 
-(Bind b) u x) (\lambda (t7: T).(ty3 g c3 t7 (THead (Bind b) u t3))) (ex_ind T 
-(\lambda (t7: T).(ty3 g (CHead c3 (Bind b) u) t3 t7)) (ty3 g c3 (THead (Bind 
-b) u x) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H13: (ty3 g (CHead 
-c3 (Bind b) u) t3 x0)).(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c 
-u c3 H8) e H9) b x t3 (H3 (S i) u0 (CHead c3 (Bind b) u) x (fsubst0_both (S 
-i) u0 (CHead c (Bind b) u) t2 x H12 (CHead c3 (Bind b) u) (csubst0_fst_bind b 
-i c c3 u0 H8 u)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H9 u)) x0 
-H13))) (ty3_correct g (CHead c3 (Bind b) u) x t3 (H3 (S i) u0 (CHead c3 (Bind 
-b) u) x (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x H12 (CHead c3 (Bind 
-b) u) (csubst0_fst_bind b i c c3 u0 H8 u)) e (getl_head (Bind b) i c (CHead e 
-(Bind Abbr) u0) H9 u)))) t6 H11)))) H10)) (\lambda (H10: (ex3_2 T T (\lambda 
-(u2: T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7: 
-T).(subst0 (s (Bind b) i) u0 t2 t7))))).(ex3_2_ind T T (\lambda (u2: 
-T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7: 
-T).(subst0 (s (Bind b) i) u0 t2 t7))) (ty3 g c3 t6 (THead (Bind b) u t3)) 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (H11: (eq T t6 (THead (Bind b) x0 
-x1))).(\lambda (H12: (subst0 i u0 u x0)).(\lambda (H13: (subst0 (s (Bind b) 
-i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t7: T).(ty3 g c3 
-t7 (THead (Bind b) u t3))) (ex_ind T (\lambda (t7: T).(ty3 g (CHead c3 (Bind 
-b) u) t3 t7)) (ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)) 
-(\lambda (x: T).(\lambda (H14: (ty3 g (CHead c3 (Bind b) u) t3 x)).(ex_ind T 
-(\lambda (t7: T).(ty3 g (CHead c3 (Bind b) u) x t7)) (ty3 g c3 (THead (Bind 
-b) x0 x1) (THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (H15: (ty3 g 
-(CHead c3 (Bind b) u) x x2)).(ex_ind T (\lambda (t7: T).(ty3 g (CHead c3 
-(Bind b) x0) t3 t7)) (ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)) 
-(\lambda (x3: T).(\lambda (H16: (ty3 g (CHead c3 (Bind b) x0) t3 
-x3)).(ty3_conv g c3 (THead (Bind b) u t3) (THead (Bind b) u x) (ty3_bind g c3 
-u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H8) e H9) b t3 x H14 x2 H15) 
-(THead (Bind b) x0 x1) (THead (Bind b) x0 t3) (ty3_bind g c3 x0 t0 (H1 i u0 
-c3 x0 (fsubst0_both i u0 c u x0 H12 c3 H8) e H9) b x1 t3 (H3 (S i) u0 (CHead 
-c3 (Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 H13 
-(CHead c3 (Bind b) x0) (csubst0_both_bind b i u0 u x0 H12 c c3 H8)) e 
-(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H9 u)) x3 H16) (pc3_fsubst0 
-c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c (THead (Bind b) u 
+(Bind b) x) (csubst0_both_bind b i u0 u x H10 c c3 H6)) e (getl_head (Bind b) 
+i c (CHead e (Bind Abbr) u0) H7 u))) (pc3_fsubst0 c (THead (Bind b) u t3) 
+(THead (Bind b) u t3) (pc3_refl c (THead (Bind b) u t3)) i u0 c3 (THead (Bind 
+b) x t3) (fsubst0_both i u0 c (THead (Bind b) u t3) (THead (Bind b) x t3) 
+(subst0_fst u0 x u i H10 t3 (Bind b)) c3 H6) e H7)))) (ty3_correct g (CHead 
+c3 (Bind b) x) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) x) t2 (fsubst0_fst (S i) 
+u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) x) (csubst0_both_bind b i u0 u 
+x H10 c c3 H6)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H7 u)))))) 
+(ty3_correct g (CHead c3 (Bind b) u) t3 x0 H11)))) (ty3_correct g (CHead c3 
+(Bind b) u) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 
+(CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 
+H6 u)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H7 u)))) t5 H9)))) 
+H8)) (\lambda (H8: (ex2 T (\lambda (t6: T).(eq T t5 (THead (Bind b) u t6))) 
+(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6)))).(ex2_ind T (\lambda (t6: 
+T).(eq T t5 (THead (Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) 
+u0 t2 t6)) (ty3 g c3 t5 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H9: 
+(eq T t5 (THead (Bind b) u x))).(\lambda (H10: (subst0 (s (Bind b) i) u0 t2 
+x)).(eq_ind_r T (THead (Bind b) u x) (\lambda (t6: T).(ty3 g c3 t6 (THead 
+(Bind b) u t3))) (ex_ind T (\lambda (t6: T).(ty3 g (CHead c3 (Bind b) u) t3 
+t6)) (ty3 g c3 (THead (Bind b) u x) (THead (Bind b) u t3)) (\lambda (x0: 
+T).(\lambda (_: (ty3 g (CHead c3 (Bind b) u) t3 x0)).(ty3_bind g c3 u t0 (H1 
+i u0 c3 u (fsubst0_fst i u0 c u c3 H6) e H7) b x t3 (H3 (S i) u0 (CHead c3 
+(Bind b) u) x (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x H10 (CHead c3 
+(Bind b) u) (csubst0_fst_bind b i c c3 u0 H6 u)) e (getl_head (Bind b) i c 
+(CHead e (Bind Abbr) u0) H7 u))))) (ty3_correct g (CHead c3 (Bind b) u) x t3 
+(H3 (S i) u0 (CHead c3 (Bind b) u) x (fsubst0_both (S i) u0 (CHead c (Bind b) 
+u) t2 x H10 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 H6 u)) e 
+(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H7 u)))) t5 H9)))) H8)) 
+(\lambda (H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) 
+(\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 
+t6))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead 
+(Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2))) 
+(\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6))) (ty3 g c3 
+t5 (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H9: (eq 
+T t5 (THead (Bind b) x0 x1))).(\lambda (H10: (subst0 i u0 u x0)).(\lambda 
+(H11: (subst0 (s (Bind b) i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1) 
+(\lambda (t6: T).(ty3 g c3 t6 (THead (Bind b) u t3))) (ex_ind T (\lambda (t6: 
+T).(ty3 g (CHead c3 (Bind b) u) t3 t6)) (ty3 g c3 (THead (Bind b) x0 x1) 
+(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H12: (ty3 g (CHead c3 (Bind 
+b) u) t3 x)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead c3 (Bind b) u) x t6)) 
+(ty3 g c3 (THead (Bind b) x0 x1) (THead (Bind b) u t3)) (\lambda (x2: 
+T).(\lambda (_: (ty3 g (CHead c3 (Bind b) u) x x2)).(ex_ind T (\lambda (t6: 
+T).(ty3 g (CHead c3 (Bind b) x0) t3 t6)) (ty3 g c3 (THead (Bind b) x0 x1) 
+(THead (Bind b) u t3)) (\lambda (x3: T).(\lambda (_: (ty3 g (CHead c3 (Bind 
+b) x0) t3 x3)).(ty3_conv g c3 (THead (Bind b) u t3) (THead (Bind b) u x) 
+(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H6) e H7) b t3 x 
+H12) (THead (Bind b) x0 x1) (THead (Bind b) x0 t3) (ty3_bind g c3 x0 t0 (H1 i 
+u0 c3 x0 (fsubst0_both i u0 c u x0 H10 c3 H6) e H7) b x1 t3 (H3 (S i) u0 
+(CHead c3 (Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 
+H11 (CHead c3 (Bind b) x0) (csubst0_both_bind b i u0 u x0 H10 c c3 H6)) e 
+(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H7 u))) (pc3_fsubst0 c 
+(THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c (THead (Bind b) u 
 t3)) i u0 c3 (THead (Bind b) x0 t3) (fsubst0_both i u0 c (THead (Bind b) u 
-t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H12 t3 (Bind b)) c3 H8) e 
-H9)))) (ty3_correct g (CHead c3 (Bind b) x0) x1 t3 (H3 (S i) u0 (CHead c3 
-(Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 H13 (CHead 
-c3 (Bind b) x0) (csubst0_both_bind b i u0 u x0 H12 c c3 H8)) e (getl_head 
-(Bind b) i c (CHead e (Bind Abbr) u0) H9 u)))))) (ty3_correct g (CHead c3 
-(Bind b) u) t3 x H14)))) (ty3_correct g (CHead c3 (Bind b) u) t2 t3 (H3 (S i) 
+t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H10 t3 (Bind b)) c3 H6) e 
+H7)))) (ty3_correct g (CHead c3 (Bind b) x0) x1 t3 (H3 (S i) u0 (CHead c3 
+(Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 H11 (CHead 
+c3 (Bind b) x0) (csubst0_both_bind b i u0 u x0 H10 c c3 H6)) e (getl_head 
+(Bind b) i c (CHead e (Bind Abbr) u0) H7 u)))))) (ty3_correct g (CHead c3 
+(Bind b) u) t3 x H12)))) (ty3_correct g (CHead c3 (Bind b) u) t2 t3 (H3 (S i) 
 u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 
-(CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 H8 u)) e (getl_head (Bind 
-b) i c (CHead e (Bind Abbr) u0) H9 u)))) t6 H11)))))) H10)) (subst0_gen_head 
-(Bind b) u0 u t2 t6 i H7)))))))) c2 t5 H6))))))))))))))))))) (\lambda (c: 
+(CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 H6 u)) e (getl_head (Bind 
+b) i c (CHead e (Bind Abbr) u0) H7 u)))) t5 H9)))))) H8)) (subst0_gen_head 
+(Bind b) u0 u t2 t5 i H5)))))))) c2 t4 H4)))))))))))))))) (\lambda (c: 
 C).(\lambda (w: T).(\lambda (u: T).(\lambda (H0: (ty3 g c w u)).(\lambda (H1: 
 ((\forall (i: nat).(\forall (u0: T).(\forall (c2: C).(\forall (t2: 
 T).((fsubst0 i u0 c w c2 t2) \to (\forall (e: C).((getl i c (CHead e (Bind 
@@ -681,29 +673,26 @@ x v))).(\lambda (H9: (subst0 i u0 w x)).(eq_ind_r T (THead (Flat Appl) x v)
 (ex_ind T (\lambda (t4: T).(ty3 g c (THead (Bind Abst) u t0) t4)) (ty3 g c 
 (THead (Flat Appl) x v) (THead (Flat Appl) w (THead (Bind Abst) u t0))) 
 (\lambda (x0: T).(\lambda (H10: (ty3 g c (THead (Bind Abst) u t0) 
-x0)).(ex4_3_ind T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c 
-(THead (Bind Abst) u t4) x0)))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_: 
-T).(ty3 g c u t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g 
-(CHead c (Bind Abst) u) t0 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda 
-(t6: T).(ty3 g (CHead c (Bind Abst) u) t4 t6)))) (ty3 g c (THead (Flat Appl) 
-x v) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x1: 
-T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (_: (pc3 c (THead (Bind Abst) u 
+x0)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c (THead (Bind 
+Abst) u t4) x0))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c u t5))) (\lambda 
+(t4: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t0 t4))) (ty3 g c 
+(THead (Flat Appl) x v) (THead (Flat Appl) w (THead (Bind Abst) u t0))) 
+(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c (THead (Bind Abst) u 
 x1) x0)).(\lambda (_: (ty3 g c u x2)).(\lambda (H13: (ty3 g (CHead c (Bind 
-Abst) u) t0 x1)).(\lambda (H14: (ty3 g (CHead c (Bind Abst) u) x1 
-x3)).(ex_ind T (\lambda (t4: T).(ty3 g c u t4)) (ty3 g c (THead (Flat Appl) x 
-v) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x4: T).(\lambda 
-(H15: (ty3 g c u x4)).(ty3_conv g c (THead (Flat Appl) w (THead (Bind Abst) u 
-t0)) (THead (Flat Appl) w (THead (Bind Abst) u x1)) (ty3_appl g c w u H0 
-(THead (Bind Abst) u t0) x1 (ty3_bind g c u x4 H15 Abst t0 x1 H13 x3 H14)) 
-(THead (Flat Appl) x v) (THead (Flat Appl) x (THead (Bind Abst) u t0)) 
-(ty3_appl g c x u (H1 i u0 c x (fsubst0_snd i u0 c w x H9) e H6) v t0 H2) 
-(pc3_fsubst0 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat 
-Appl) w (THead (Bind Abst) u t0)) (pc3_refl c (THead (Flat Appl) w (THead 
-(Bind Abst) u t0))) i u0 c (THead (Flat Appl) x (THead (Bind Abst) u t0)) 
-(fsubst0_snd i u0 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead 
-(Flat Appl) x (THead (Bind Abst) u t0)) (subst0_fst u0 x w i H9 (THead (Bind 
-Abst) u t0) (Flat Appl))) e H6)))) (ty3_correct g c x u (H1 i u0 c x 
-(fsubst0_snd i u0 c w x H9) e H6)))))))))) (ty3_gen_bind g Abst c u t0 x0 
+Abst) u) t0 x1)).(ex_ind T (\lambda (t4: T).(ty3 g c u t4)) (ty3 g c (THead 
+(Flat Appl) x v) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda 
+(x3: T).(\lambda (H14: (ty3 g c u x3)).(ty3_conv g c (THead (Flat Appl) w 
+(THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u x1)) 
+(ty3_appl g c w u H0 (THead (Bind Abst) u t0) x1 (ty3_bind g c u x3 H14 Abst 
+t0 x1 H13)) (THead (Flat Appl) x v) (THead (Flat Appl) x (THead (Bind Abst) u 
+t0)) (ty3_appl g c x u (H1 i u0 c x (fsubst0_snd i u0 c w x H9) e H6) v t0 
+H2) (pc3_fsubst0 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead 
+(Flat Appl) w (THead (Bind Abst) u t0)) (pc3_refl c (THead (Flat Appl) w 
+(THead (Bind Abst) u t0))) i u0 c (THead (Flat Appl) x (THead (Bind Abst) u 
+t0)) (fsubst0_snd i u0 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) 
+(THead (Flat Appl) x (THead (Bind Abst) u t0)) (subst0_fst u0 x w i H9 (THead 
+(Bind Abst) u t0) (Flat Appl))) e H6)))) (ty3_correct g c x u (H1 i u0 c x 
+(fsubst0_snd i u0 c w x H9) e H6)))))))) (ty3_gen_bind g Abst c u t0 x0 
 H10)))) (ty3_correct g c v (THead (Bind Abst) u t0) H2)) t3 H8)))) H7)) 
 (\lambda (H7: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Flat Appl) w t4))) 
 (\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v t4)))).(ex2_ind T (\lambda 
@@ -727,31 +716,28 @@ u0 w x0)).(\lambda (H10: (subst0 (s (Flat Appl) i) u0 v x1)).(eq_ind_r T
 (THead (Bind Abst) u t0)))) (ex_ind T (\lambda (t4: T).(ty3 g c (THead (Bind 
 Abst) u t0) t4)) (ty3 g c (THead (Flat Appl) x0 x1) (THead (Flat Appl) w 
 (THead (Bind Abst) u t0))) (\lambda (x: T).(\lambda (H11: (ty3 g c (THead 
-(Bind Abst) u t0) x)).(ex4_3_ind T T T (\lambda (t4: T).(\lambda (_: 
-T).(\lambda (_: T).(pc3 c (THead (Bind Abst) u t4) x)))) (\lambda (_: 
-T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c u t5)))) (\lambda (t4: 
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t0 t4)))) 
-(\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c (Bind Abst) 
-u) t4 t6)))) (ty3 g c (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead 
-(Bind Abst) u t0))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: 
-T).(\lambda (_: (pc3 c (THead (Bind Abst) u x2) x)).(\lambda (_: (ty3 g c u 
-x3)).(\lambda (H14: (ty3 g (CHead c (Bind Abst) u) t0 x2)).(\lambda (H15: 
-(ty3 g (CHead c (Bind Abst) u) x2 x4)).(ex_ind T (\lambda (t4: T).(ty3 g c u 
-t4)) (ty3 g c (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind 
-Abst) u t0))) (\lambda (x5: T).(\lambda (H16: (ty3 g c u x5)).(ty3_conv g c 
-(THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead 
-(Bind Abst) u x2)) (ty3_appl g c w u H0 (THead (Bind Abst) u t0) x2 (ty3_bind 
-g c u x5 H16 Abst t0 x2 H14 x4 H15)) (THead (Flat Appl) x0 x1) (THead (Flat 
-Appl) x0 (THead (Bind Abst) u t0)) (ty3_appl g c x0 u (H1 i u0 c x0 
-(fsubst0_snd i u0 c w x0 H9) e H6) x1 t0 (H3 (s (Flat Appl) i) u0 c x1 
-(fsubst0_snd (s (Flat Appl) i) u0 c v x1 H10) e H6)) (pc3_fsubst0 c (THead 
+(Bind Abst) u t0) x)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c 
+(THead (Bind Abst) u t4) x))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c u 
+t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t0 
+t4))) (ty3 g c (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind 
+Abst) u t0))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (_: (pc3 c (THead 
+(Bind Abst) u x2) x)).(\lambda (_: (ty3 g c u x3)).(\lambda (H14: (ty3 g 
+(CHead c (Bind Abst) u) t0 x2)).(ex_ind T (\lambda (t4: T).(ty3 g c u t4)) 
+(ty3 g c (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind Abst) u 
+t0))) (\lambda (x4: T).(\lambda (H15: (ty3 g c u x4)).(ty3_conv g c (THead 
 (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind 
-Abst) u t0)) (pc3_refl c (THead (Flat Appl) w (THead (Bind Abst) u t0))) i u0 
-c (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) (fsubst0_snd i u0 c (THead 
-(Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) x0 (THead (Bind 
-Abst) u t0)) (subst0_fst u0 x0 w i H9 (THead (Bind Abst) u t0) (Flat Appl))) 
-e H6)))) (ty3_correct g c w u H0))))))))) (ty3_gen_bind g Abst c u t0 x 
-H11)))) (ty3_correct g c v (THead (Bind Abst) u t0) H2)) t3 H8)))))) H7)) 
+Abst) u x2)) (ty3_appl g c w u H0 (THead (Bind Abst) u t0) x2 (ty3_bind g c u 
+x4 H15 Abst t0 x2 H14)) (THead (Flat Appl) x0 x1) (THead (Flat Appl) x0 
+(THead (Bind Abst) u t0)) (ty3_appl g c x0 u (H1 i u0 c x0 (fsubst0_snd i u0 
+c w x0 H9) e H6) x1 t0 (H3 (s (Flat Appl) i) u0 c x1 (fsubst0_snd (s (Flat 
+Appl) i) u0 c v x1 H10) e H6)) (pc3_fsubst0 c (THead (Flat Appl) w (THead 
+(Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u t0)) (pc3_refl c 
+(THead (Flat Appl) w (THead (Bind Abst) u t0))) i u0 c (THead (Flat Appl) x0 
+(THead (Bind Abst) u t0)) (fsubst0_snd i u0 c (THead (Flat Appl) w (THead 
+(Bind Abst) u t0)) (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) 
+(subst0_fst u0 x0 w i H9 (THead (Bind Abst) u t0) (Flat Appl))) e H6)))) 
+(ty3_correct g c w u H0))))))) (ty3_gen_bind g Abst c u t0 x H11)))) 
+(ty3_correct g c v (THead (Bind Abst) u t0) H2)) t3 H8)))))) H7)) 
 (subst0_gen_head (Flat Appl) u0 w v t3 i H5)))))) (\lambda (c3: C).(\lambda 
 (H5: (csubst0 i u0 c c3)).(\lambda (e: C).(\lambda (H6: (getl i c (CHead e 
 (Bind Abbr) u0))).(ty3_appl g c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 
@@ -774,83 +760,76 @@ Appl) w (THead (Bind Abst) u t0))) (\lambda (x: T).(\lambda (H9: (eq T t3
 (THead (Bind Abst) u t0)))) (ex_ind T (\lambda (t4: T).(ty3 g c3 (THead (Bind 
 Abst) u t0) t4)) (ty3 g c3 (THead (Flat Appl) x v) (THead (Flat Appl) w 
 (THead (Bind Abst) u t0))) (\lambda (x0: T).(\lambda (H11: (ty3 g c3 (THead 
-(Bind Abst) u t0) x0)).(ex4_3_ind T T T (\lambda (t4: T).(\lambda (_: 
-T).(\lambda (_: T).(pc3 c3 (THead (Bind Abst) u t4) x0)))) (\lambda (_: 
-T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c3 u t5)))) (\lambda (t4: 
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c3 (Bind Abst) u) t0 t4)))) 
-(\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c3 (Bind 
-Abst) u) t4 t6)))) (ty3 g c3 (THead (Flat Appl) x v) (THead (Flat Appl) w 
-(THead (Bind Abst) u t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: 
-T).(\lambda (_: (pc3 c3 (THead (Bind Abst) u x1) x0)).(\lambda (H13: (ty3 g 
-c3 u x2)).(\lambda (H14: (ty3 g (CHead c3 (Bind Abst) u) t0 x1)).(\lambda 
-(H15: (ty3 g (CHead c3 (Bind Abst) u) x1 x3)).(ty3_conv g c3 (THead (Flat 
-Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u 
-x1)) (ty3_appl g c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 H6) e H7) 
-(THead (Bind Abst) u t0) x1 (ty3_bind g c3 u x2 H13 Abst t0 x1 H14 x3 H15)) 
-(THead (Flat Appl) x v) (THead (Flat Appl) x (THead (Bind Abst) u t0)) 
-(ty3_appl g c3 x u (H1 i u0 c3 x (fsubst0_both i u0 c w x H10 c3 H6) e H7) v 
-t0 (H3 i u0 c3 v (fsubst0_fst i u0 c v c3 H6) e H7)) (pc3_fsubst0 c (THead 
-(Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind 
-Abst) u t0)) (pc3_refl c (THead (Flat Appl) w (THead (Bind Abst) u t0))) i u0 
-c3 (THead (Flat Appl) x (THead (Bind Abst) u t0)) (fsubst0_both i u0 c (THead 
-(Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) x (THead (Bind 
-Abst) u t0)) (subst0_fst u0 x w i H10 (THead (Bind Abst) u t0) (Flat Appl)) 
-c3 H6) e H7))))))))) (ty3_gen_bind g Abst c3 u t0 x0 H11)))) (ty3_correct g 
-c3 v (THead (Bind Abst) u t0) (H3 i u0 c3 v (fsubst0_fst i u0 c v c3 H6) e 
-H7))) t3 H9)))) H8)) (\lambda (H8: (ex2 T (\lambda (t4: T).(eq T t3 (THead 
-(Flat Appl) w t4))) (\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v 
-t4)))).(ex2_ind T (\lambda (t4: T).(eq T t3 (THead (Flat Appl) w t4))) 
-(\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v t4)) (ty3 g c3 t3 (THead 
-(Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x: T).(\lambda (H9: (eq T 
-t3 (THead (Flat Appl) w x))).(\lambda (H10: (subst0 (s (Flat Appl) i) u0 v 
-x)).(eq_ind_r T (THead (Flat Appl) w x) (\lambda (t4: T).(ty3 g c3 t4 (THead 
-(Flat Appl) w (THead (Bind Abst) u t0)))) (ty3_appl g c3 w u (H1 i u0 c3 w 
-(fsubst0_fst i u0 c w c3 H6) e H7) x t0 (H3 i u0 c3 x (fsubst0_both i u0 c v 
-x H10 c3 H6) e H7)) t3 H9)))) H8)) (\lambda (H8: (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 w u2))) (\lambda (_: T).(\lambda (t4: 
-T).(subst0 (s (Flat Appl) i) u0 v t4))))).(ex3_2_ind T T (\lambda (u2: 
-T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i u0 w u2))) (\lambda (_: T).(\lambda (t4: 
-T).(subst0 (s (Flat Appl) i) u0 v t4))) (ty3 g c3 t3 (THead (Flat Appl) w 
-(THead (Bind Abst) u t0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H9: 
-(eq T t3 (THead (Flat Appl) x0 x1))).(\lambda (H10: (subst0 i u0 w 
-x0)).(\lambda (H11: (subst0 (s (Flat Appl) i) u0 v x1)).(eq_ind_r T (THead 
-(Flat Appl) x0 x1) (\lambda (t4: T).(ty3 g c3 t4 (THead (Flat Appl) w (THead 
-(Bind Abst) u t0)))) (ex_ind T (\lambda (t4: T).(ty3 g c3 (THead (Bind Abst) 
-u t0) t4)) (ty3 g c3 (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead 
-(Bind Abst) u t0))) (\lambda (x: T).(\lambda (H12: (ty3 g c3 (THead (Bind 
-Abst) u t0) x)).(ex4_3_ind T T T (\lambda (t4: T).(\lambda (_: T).(\lambda 
-(_: T).(pc3 c3 (THead (Bind Abst) u t4) x)))) (\lambda (_: T).(\lambda (t5: 
-T).(\lambda (_: T).(ty3 g c3 u t5)))) (\lambda (t4: T).(\lambda (_: 
-T).(\lambda (_: T).(ty3 g (CHead c3 (Bind Abst) u) t0 t4)))) (\lambda (t4: 
-T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c3 (Bind Abst) u) t4 t6)))) 
+(Bind Abst) u t0) x0)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 
+c3 (THead (Bind Abst) u t4) x0))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c3 
+u t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c3 (Bind Abst) u) t0 
+t4))) (ty3 g c3 (THead (Flat Appl) x v) (THead (Flat Appl) w (THead (Bind 
+Abst) u t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c3 (THead 
+(Bind Abst) u x1) x0)).(\lambda (H13: (ty3 g c3 u x2)).(\lambda (H14: (ty3 g 
+(CHead c3 (Bind Abst) u) t0 x1)).(ty3_conv g c3 (THead (Flat Appl) w (THead 
+(Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u x1)) (ty3_appl g 
+c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 H6) e H7) (THead (Bind Abst) u 
+t0) x1 (ty3_bind g c3 u x2 H13 Abst t0 x1 H14)) (THead (Flat Appl) x v) 
+(THead (Flat Appl) x (THead (Bind Abst) u t0)) (ty3_appl g c3 x u (H1 i u0 c3 
+x (fsubst0_both i u0 c w x H10 c3 H6) e H7) v t0 (H3 i u0 c3 v (fsubst0_fst i 
+u0 c v c3 H6) e H7)) (pc3_fsubst0 c (THead (Flat Appl) w (THead (Bind Abst) u 
+t0)) (THead (Flat Appl) w (THead (Bind Abst) u t0)) (pc3_refl c (THead (Flat 
+Appl) w (THead (Bind Abst) u t0))) i u0 c3 (THead (Flat Appl) x (THead (Bind 
+Abst) u t0)) (fsubst0_both i u0 c (THead (Flat Appl) w (THead (Bind Abst) u 
+t0)) (THead (Flat Appl) x (THead (Bind Abst) u t0)) (subst0_fst u0 x w i H10 
+(THead (Bind Abst) u t0) (Flat Appl)) c3 H6) e H7))))))) (ty3_gen_bind g Abst 
+c3 u t0 x0 H11)))) (ty3_correct g c3 v (THead (Bind Abst) u t0) (H3 i u0 c3 v 
+(fsubst0_fst i u0 c v c3 H6) e H7))) t3 H9)))) H8)) (\lambda (H8: (ex2 T 
+(\lambda (t4: T).(eq T t3 (THead (Flat Appl) w t4))) (\lambda (t4: T).(subst0 
+(s (Flat Appl) i) u0 v t4)))).(ex2_ind T (\lambda (t4: T).(eq T t3 (THead 
+(Flat Appl) w t4))) (\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v t4)) (ty3 
+g c3 t3 (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x: 
+T).(\lambda (H9: (eq T t3 (THead (Flat Appl) w x))).(\lambda (H10: (subst0 (s 
+(Flat Appl) i) u0 v x)).(eq_ind_r T (THead (Flat Appl) w x) (\lambda (t4: 
+T).(ty3 g c3 t4 (THead (Flat Appl) w (THead (Bind Abst) u t0)))) (ty3_appl g 
+c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 H6) e H7) x t0 (H3 i u0 c3 x 
+(fsubst0_both i u0 c v x H10 c3 H6) e H7)) t3 H9)))) H8)) (\lambda (H8: 
+(ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 
+t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 w u2))) (\lambda (_: 
+T).(\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v t4))))).(ex3_2_ind T T 
+(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 i u0 w u2))) (\lambda (_: 
+T).(\lambda (t4: T).(subst0 (s (Flat Appl) i) u0 v t4))) (ty3 g c3 t3 (THead 
+(Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x0: T).(\lambda (x1: 
+T).(\lambda (H9: (eq T t3 (THead (Flat Appl) x0 x1))).(\lambda (H10: (subst0 
+i u0 w x0)).(\lambda (H11: (subst0 (s (Flat Appl) i) u0 v x1)).(eq_ind_r T 
+(THead (Flat Appl) x0 x1) (\lambda (t4: T).(ty3 g c3 t4 (THead (Flat Appl) w 
+(THead (Bind Abst) u t0)))) (ex_ind T (\lambda (t4: T).(ty3 g c3 (THead (Bind 
+Abst) u t0) t4)) (ty3 g c3 (THead (Flat Appl) x0 x1) (THead (Flat Appl) w 
+(THead (Bind Abst) u t0))) (\lambda (x: T).(\lambda (H12: (ty3 g c3 (THead 
+(Bind Abst) u t0) x)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c3 
+(THead (Bind Abst) u t4) x))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c3 u 
+t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c3 (Bind Abst) u) t0 
+t4))) (ty3 g c3 (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind 
+Abst) u t0))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (_: (pc3 c3 (THead 
+(Bind Abst) u x2) x)).(\lambda (_: (ty3 g c3 u x3)).(\lambda (H15: (ty3 g 
+(CHead c3 (Bind Abst) u) t0 x2)).(ex_ind T (\lambda (t4: T).(ty3 g c3 u t4)) 
 (ty3 g c3 (THead (Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind Abst) u 
-t0))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (_: (pc3 c3 
-(THead (Bind Abst) u x2) x)).(\lambda (_: (ty3 g c3 u x3)).(\lambda (H15: 
-(ty3 g (CHead c3 (Bind Abst) u) t0 x2)).(\lambda (H16: (ty3 g (CHead c3 (Bind 
-Abst) u) x2 x4)).(ex_ind T (\lambda (t4: T).(ty3 g c3 u t4)) (ty3 g c3 (THead 
-(Flat Appl) x0 x1) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda 
-(x5: T).(\lambda (H17: (ty3 g c3 u x5)).(ty3_conv g c3 (THead (Flat Appl) w 
-(THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u x2)) 
-(ty3_appl g c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 H6) e H7) (THead 
-(Bind Abst) u t0) x2 (ty3_bind g c3 u x5 H17 Abst t0 x2 H15 x4 H16)) (THead 
-(Flat Appl) x0 x1) (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) (ty3_appl 
-g c3 x0 u (H1 i u0 c3 x0 (fsubst0_both i u0 c w x0 H10 c3 H6) e H7) x1 t0 (H3 
-i u0 c3 x1 (fsubst0_both i u0 c v x1 H11 c3 H6) e H7)) (pc3_fsubst0 c (THead 
+t0))) (\lambda (x4: T).(\lambda (H16: (ty3 g c3 u x4)).(ty3_conv g c3 (THead 
 (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind 
-Abst) u t0)) (pc3_refl c (THead (Flat Appl) w (THead (Bind Abst) u t0))) i u0 
-c3 (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) (fsubst0_both i u0 c 
-(THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) x0 (THead 
-(Bind Abst) u t0)) (subst0_fst u0 x0 w i H10 (THead (Bind Abst) u t0) (Flat 
-Appl)) c3 H6) e H7)))) (ty3_correct g c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 
-c w c3 H6) e H7)))))))))) (ty3_gen_bind g Abst c3 u t0 x H12)))) (ty3_correct 
-g c3 v (THead (Bind Abst) u t0) (H3 i u0 c3 v (fsubst0_fst i u0 c v c3 H6) e 
-H7))) t3 H9)))))) H8)) (subst0_gen_head (Flat Appl) u0 w v t3 i H5)))))))) c2 
-t2 H4))))))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda (t3: 
-T).(\lambda (H0: (ty3 g c t2 t3)).(\lambda (H1: ((\forall (i: nat).(\forall 
-(u: T).(\forall (c2: C).(\forall (t4: T).((fsubst0 i u c t2 c2 t4) \to 
-(\forall (e: C).((getl i c (CHead e (Bind Abbr) u)) \to (ty3 g c2 t4 
+Abst) u x2)) (ty3_appl g c3 w u (H1 i u0 c3 w (fsubst0_fst i u0 c w c3 H6) e 
+H7) (THead (Bind Abst) u t0) x2 (ty3_bind g c3 u x4 H16 Abst t0 x2 H15)) 
+(THead (Flat Appl) x0 x1) (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) 
+(ty3_appl g c3 x0 u (H1 i u0 c3 x0 (fsubst0_both i u0 c w x0 H10 c3 H6) e H7) 
+x1 t0 (H3 i u0 c3 x1 (fsubst0_both i u0 c v x1 H11 c3 H6) e H7)) (pc3_fsubst0 
+c (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead 
+(Bind Abst) u t0)) (pc3_refl c (THead (Flat Appl) w (THead (Bind Abst) u 
+t0))) i u0 c3 (THead (Flat Appl) x0 (THead (Bind Abst) u t0)) (fsubst0_both i 
+u0 c (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) x0 
+(THead (Bind Abst) u t0)) (subst0_fst u0 x0 w i H10 (THead (Bind Abst) u t0) 
+(Flat Appl)) c3 H6) e H7)))) (ty3_correct g c3 w u (H1 i u0 c3 w (fsubst0_fst 
+i u0 c w c3 H6) e H7)))))))) (ty3_gen_bind g Abst c3 u t0 x H12)))) 
+(ty3_correct g c3 v (THead (Bind Abst) u t0) (H3 i u0 c3 v (fsubst0_fst i u0 
+c v c3 H6) e H7))) t3 H9)))))) H8)) (subst0_gen_head (Flat Appl) u0 w v t3 i 
+H5)))))))) c2 t2 H4))))))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda 
+(t3: T).(\lambda (H0: (ty3 g c t2 t3)).(\lambda (H1: ((\forall (i: 
+nat).(\forall (u: T).(\forall (c2: C).(\forall (t4: T).((fsubst0 i u c t2 c2 
+t4) \to (\forall (e: C).((getl i c (CHead e (Bind Abbr) u)) \to (ty3 g c2 t4 
 t3)))))))))).(\lambda (t0: T).(\lambda (H2: (ty3 g c t3 t0)).(\lambda (H3: 
 ((\forall (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t4: 
 T).((fsubst0 i u c t3 c2 t4) \to (\forall (e: C).((getl i c (CHead e (Bind 
@@ -858,99 +837,130 @@ Abbr) u)) \to (ty3 g c2 t4 t0)))))))))).(\lambda (i: nat).(\lambda (u:
 T).(\lambda (c2: C).(\lambda (t4: T).(\lambda (H4: (fsubst0 i u c (THead 
 (Flat Cast) t3 t2) c2 t4)).(fsubst0_ind i u c (THead (Flat Cast) t3 t2) 
 (\lambda (c0: C).(\lambda (t5: T).(\forall (e: C).((getl i c (CHead e (Bind 
-Abbr) u)) \to (ty3 g c0 t5 t3))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u 
-(THead (Flat Cast) t3 t2) t5)).(\lambda (e: C).(\lambda (H6: (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 c t5 t3) (\lambda (H7: (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 
+Abbr) u)) \to (ty3 g c0 t5 (THead (Flat Cast) t0 t3)))))) (\lambda (t5: 
+T).(\lambda (H5: (subst0 i u (THead (Flat Cast) t3 t2) t5)).(\lambda (e: 
+C).(\lambda (H6: (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)) (ty3 g c t5 t3) (\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Flat 
-Cast) x t2))).(\lambda (H9: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat Cast) 
-x t2) (\lambda (t6: T).(ty3 g c t6 t3)) (ty3_conv g c t3 t0 H2 (THead (Flat 
-Cast) x t2) x (ty3_cast g c t2 x (ty3_conv g c x t0 (H3 i u c x (fsubst0_snd 
-i u c t3 x H9) e H6) t2 t3 H0 (pc3_s c t3 x (pc3_fsubst0 c t3 t3 (pc3_refl c 
-t3) i u c x (fsubst0_snd i u c t3 x H9) e H6))) t0 (H3 i u c x (fsubst0_snd i 
-u c t3 x H9) e H6)) (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x (fsubst0_snd 
-i u c t3 x H9) e H6)) t5 H8)))) H7)) (\lambda (H7: (ex2 T (\lambda (t6: 
-T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat 
-Cast) i) u t2 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Flat Cast) 
-t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c t5 t3) 
-(\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Flat Cast) t3 x))).(\lambda 
-(H9: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead (Flat Cast) t3 x) 
-(\lambda (t6: T).(ty3 g c t6 t3)) (ty3_cast g c x t3 (H1 (s (Flat Cast) i) u 
-c x (fsubst0_snd (s (Flat Cast) i) u c t2 x H9) e H6) t0 H2) t5 H8)))) H7)) 
+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 c t5 (THead (Flat Cast) t0 
+t3)) (\lambda (H7: (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 
+c t5 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H8: (eq T t5 (THead 
+(Flat Cast) x t2))).(\lambda (H9: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat 
+Cast) x t2) (\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) x t2) (THead 
+(Flat Cast) t0 t3)) (\lambda (x0: T).(\lambda (H10: (ty3 g c t0 
+x0)).(ty3_conv g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0) 
+(ty3_cast g c t3 t0 H2 x0 H10) (THead (Flat Cast) x t2) (THead (Flat Cast) t0 
+x) (ty3_cast g c t2 x (ty3_conv g c x t0 (H3 i u c x (fsubst0_snd i u c t3 x 
+H9) e H6) t2 t3 H0 (pc3_s c t3 x (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x 
+(fsubst0_snd i u c t3 x H9) e H6))) t0 (H3 i u c x (fsubst0_snd i u c t3 x 
+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 x) 
+(fsubst0_snd i u c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x) 
+(subst0_snd (Flat Cast) u x t3 i H9 t0)) e H6)))) (ty3_correct g c x t0 (H3 i 
+u c x (fsubst0_snd i u c t3 x H9) e H6))) t5 H8)))) H7)) (\lambda (H7: (ex2 T 
+(\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: 
+T).(subst0 (s (Flat Cast) i) u t2 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 
+(THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 
+t6)) (ty3 g c t5 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H8: (eq 
+T t5 (THead (Flat Cast) t3 x))).(\lambda (H9: (subst0 (s (Flat Cast) i) u t2 
+x)).(eq_ind_r T (THead (Flat Cast) t3 x) (\lambda (t6: T).(ty3 g c t6 (THead 
+(Flat Cast) t0 t3))) (ty3_cast g c x t3 (H1 (s (Flat Cast) i) u c x 
+(fsubst0_snd (s (Flat Cast) i) u c t2 x H9) e H6) t0 H2) t5 H8)))) H7)) 
 (\lambda (H7: (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))))).(ex3_2_ind 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 
-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 
 t2))).(\lambda (H10: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat Cast) x t2) 
-(\lambda (t6: T).(ty3 g c3 t6 t3)) (ty3_conv g c3 t3 t0 (H3 i u c3 t3 
-(fsubst0_fst i u c t3 c3 H6) e H7) (THead (Flat Cast) x t2) x (ty3_cast g c3 
-t2 x (ty3_conv g c3 x t0 (H3 i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e 
-H7) t2 t3 (H1 i u c3 t2 (fsubst0_fst i u c t2 c3 H6) e H7) (pc3_s c3 t3 x 
-(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 
-H6) e H7))) t0 (H3 i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7)) 
-(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 
-H6) e H7)) t5 H9)))) H8)) (\lambda (H8: (ex2 T (\lambda (t6: T).(eq T t5 
-(THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 
+(\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) (ex_ind T (\lambda 
+(t6: T).(ty3 g c3 t0 t6)) (ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat 
+Cast) t0 t3)) (\lambda (x0: T).(\lambda (H11: (ty3 g c3 t0 x0)).(ty3_conv g 
+c3 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0) (ty3_cast g c3 t3 t0 
+(H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7) x0 H11) (THead (Flat Cast) x 
+t2) (THead (Flat Cast) t0 x) (ty3_cast g c3 t2 x (ty3_conv g c3 x t0 (H3 i u 
+c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7) t2 t3 (H1 i u c3 t2 
+(fsubst0_fst i u c t2 c3 H6) e H7) (pc3_s c3 t3 x (pc3_fsubst0 c t3 t3 
+(pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7))) t0 (H3 i 
+u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7)) (pc3_fsubst0 c (THead (Flat 
+Cast) t0 t3) (THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat Cast) t0 t3)) 
+i u c3 (THead (Flat Cast) t0 x) (fsubst0_both i u c (THead (Flat Cast) t0 t3) 
+(THead (Flat Cast) t0 x) (subst0_snd (Flat Cast) u x t3 i H10 t0) c3 H6) e 
+H7)))) (ty3_correct g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e 
+H7))) t5 H9)))) H8)) (\lambda (H8: (ex2 T (\lambda (t6: T).(eq T t5 (THead 
+(Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 
 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) 
-(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c3 t5 t3) 
-(\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) t3 x))).(\lambda 
-(H10: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead (Flat Cast) t3 x) 
-(\lambda (t6: T).(ty3 g c3 t6 t3)) (ty3_cast g c3 x t3 (H1 i u c3 x 
-(fsubst0_both i u c t2 x H10 c3 H6) e H7) t0 (H3 i u c3 t3 (fsubst0_fst i u c 
-t3 c3 H6) e H7)) t5 H9)))) H8)) (\lambda (H8: (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))))).(ex3_2_ind 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 (x0: 
-T).(\lambda (x1: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x0 
-x1))).(\lambda (H10: (subst0 i u t3 x0)).(\lambda (H11: (subst0 (s (Flat 
-Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t6: 
-T).(ty3 g c3 t6 t3)) (ty3_conv g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 
-c3 H6) e H7) (THead (Flat Cast) x0 x1) x0 (ty3_cast g c3 x1 x0 (ty3_conv g c3 
-x0 t0 (H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7) x1 t3 (H1 i u 
-c3 x1 (fsubst0_both i u c t2 x1 H11 c3 H6) e H7) (pc3_s c3 t3 x0 (pc3_fsubst0 
-c t3 t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e 
-H7))) t0 (H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7)) 
-(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 
-c3 H6) e H7)) t5 H9)))))) H8)) (subst0_gen_head (Flat Cast) u t3 t2 t5 i 
-H5)))))))) c2 t4 H4)))))))))))))) c1 t1 t H))))).
+(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c3 t5 (THead 
+(Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) 
+t3 x))).(\lambda (H10: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead 
+(Flat Cast) t3 x) (\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) 
+(ty3_cast g c3 x t3 (H1 i u c3 x (fsubst0_both i u c t2 x H10 c3 H6) e H7) t0 
+(H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7)) t5 H9)))) H8)) (\lambda 
+(H8: (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))))).(ex3_2_ind 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 (x0: T).(\lambda (x1: T).(\lambda (H9: (eq T t5 
+(THead (Flat Cast) x0 x1))).(\lambda (H10: (subst0 i u t3 x0)).(\lambda (H11: 
+(subst0 (s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) 
+(\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) (ex_ind T (\lambda 
+(t6: T).(ty3 g c3 t0 t6)) (ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat 
+Cast) t0 t3)) (\lambda (x: T).(\lambda (H12: (ty3 g c3 t0 x)).(ty3_conv g c3 
+(THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) (ty3_cast g c3 t3 t0 (H3 i 
+u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7) x H12) (THead (Flat Cast) x0 x1) 
+(THead (Flat Cast) t0 x0) (ty3_cast g c3 x1 x0 (ty3_conv g c3 x0 t0 (H3 i u 
+c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7) x1 t3 (H1 i u c3 x1 
+(fsubst0_both i u c t2 x1 H11 c3 H6) e H7) (pc3_s c3 t3 x0 (pc3_fsubst0 c t3 
+t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7))) t0 
+(H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7)) (pc3_fsubst0 c 
+(THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat 
+Cast) t0 t3)) i u c3 (THead (Flat Cast) t0 x0) (fsubst0_both i u c (THead 
+(Flat Cast) t0 t3) (THead (Flat Cast) t0 x0) (subst0_snd (Flat Cast) u x0 t3 
+i H10 t0) c3 H6) e H7)))) (ty3_correct g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst 
+i u c t3 c3 H6) e H7))) t5 H9)))))) H8)) (subst0_gen_head (Flat Cast) u t3 t2 
+t5 i H5)))))))) c2 t4 H4)))))))))))))) c1 t1 t H))))).
 
 theorem ty3_csubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1