X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fty3%2Ffsubst0.ma;h=d6d6beb926c530ad90777f157278e259ea93b365;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=f92366a26373a5f25736f4976b80e0fc8bc432db;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/fsubst0.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/fsubst0.ma
index f92366a26..d6d6beb92 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/fsubst0.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/fsubst0.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ty3/props.ma".
+include "basic_1/ty3/props.ma".
 
-include "Basic-1/pc3/fsubst0.ma".
+include "basic_1/pc3/fsubst0.ma".
 
-include "Basic-1/getl/getl.ma".
+include "basic_1/getl/getl.ma".
 
-theorem ty3_fsubst0:
+lemma ty3_fsubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1 
 t1 t) \to (\forall (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: 
 T).((fsubst0 i u c1 t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind 
@@ -83,45 +83,44 @@ T).(ty3 g c t4 (lift (S n) O t0))) (let H8 \def (eq_ind_r nat i (\lambda (n0:
 nat).(getl n0 c (CHead e (Bind Abbr) u0))) H5 n H6) in (let H9 \def (eq_ind C 
 (CHead d (Bind Abbr) u) (\lambda (c0: C).(getl n c c0)) H0 (CHead e (Bind 
 Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) n H0 (CHead e (Bind Abbr) u0) 
-H8)) in (let H10 \def (f_equal C C (\lambda (e0: C).(match e0 in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow 
-c0])) (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0) (getl_mono c (CHead d 
-(Bind Abbr) u) n H0 (CHead e (Bind Abbr) u0) H8)) in ((let H11 \def (f_equal 
-C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) 
-\Rightarrow u | (CHead _ _ t4) \Rightarrow t4])) (CHead d (Bind Abbr) u) 
+H8)) in (let H10 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) 
 (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) n H0 (CHead e 
-(Bind Abbr) u0) H8)) in (\lambda (H12: (eq C d e)).(let H13 \def (eq_ind_r C 
-e (\lambda (c0: C).(getl n c (CHead c0 (Bind Abbr) u0))) H9 d H12) in (let 
-H14 \def (eq_ind_r T u0 (\lambda (t4: T).(getl n c (CHead d (Bind Abbr) t4))) 
-H13 u H11) in (eq_ind T u (\lambda (t4: T).(ty3 g c (lift (S n) O t4) (lift 
-(S n) O t0))) (ty3_lift g d u t0 H1 c O (S n) (getl_drop Abbr c d u n H14)) 
-u0 H11))))) H10)))) t3 H7))) (subst0_gen_lref u0 t3 i n H4)))))) (\lambda 
-(c3: C).(\lambda (H4: (csubst0 i u0 c c3)).(\lambda (e: C).(\lambda (H5: 
-(getl i c (CHead e (Bind Abbr) u0))).(lt_le_e n i (ty3 g c3 (TLRef n) (lift 
-(S n) O t0)) (\lambda (H6: (lt n i)).(let H7 \def (csubst0_getl_lt i n H6 c 
-c3 u0 H4 (CHead d (Bind Abbr) u) H0) in (or4_ind (getl n c3 (CHead d (Bind 
-Abbr) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: 
-T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) 
-(\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 
-(CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: C).(\lambda (u1: 
-T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) (ex3_4 B C C T 
-(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C 
-(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda 
-(_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 (CHead e2 (Bind b) 
-u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: 
-T).(csubst0 (minus i (S n)) u0 e1 e2)))))) (ex4_5 B C C T T (\lambda (b: 
-B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(eq C 
-(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda (b: B).(\lambda 
-(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 (CHead e2 
-(Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: C).(\lambda 
-(u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) (\lambda (_: 
-B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 
-(minus i (S n)) u0 e1 e2))))))) (ty3 g c3 (TLRef n) (lift (S n) O t0)) 
-(\lambda (H8: (getl n c3 (CHead d (Bind Abbr) u))).(ty3_abbr g n c3 d u H8 t0 
-H1)) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda 
-(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) 
-u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: 
-T).(getl n c3 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: 
+(Bind Abbr) u0) H8)) in ((let H11 \def (f_equal C T (\lambda (e0: C).(match 
+e0 with [(CSort _) \Rightarrow u | (CHead _ _ t4) \Rightarrow t4])) (CHead d 
+(Bind Abbr) u) (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) 
+n H0 (CHead e (Bind Abbr) u0) H8)) in (\lambda (H12: (eq C d e)).(let H13 
+\def (eq_ind_r C e (\lambda (c0: C).(getl n c (CHead c0 (Bind Abbr) u0))) H9 
+d H12) in (let H14 \def (eq_ind_r T u0 (\lambda (t4: T).(getl n c (CHead d 
+(Bind Abbr) t4))) H13 u H11) in (eq_ind T u (\lambda (t4: T).(ty3 g c (lift 
+(S n) O t4) (lift (S n) O t0))) (ty3_lift g d u t0 H1 c O (S n) (getl_drop 
+Abbr c d u n H14)) u0 H11))))) H10)))) t3 H7))) (subst0_gen_lref u0 t3 i n 
+H4)))))) (\lambda (c3: C).(\lambda (H4: (csubst0 i u0 c c3)).(\lambda (e: 
+C).(\lambda (H5: (getl i c (CHead e (Bind Abbr) u0))).(lt_le_e n i (ty3 g c3 
+(TLRef n) (lift (S n) O t0)) (\lambda (H6: (lt n i)).(let H7 \def 
+(csubst0_getl_lt i n H6 c c3 u0 H4 (CHead d (Bind Abbr) u) H0) in (or4_ind 
+(getl n c3 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda 
+(e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead 
+e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: 
+T).(\lambda (w: T).(getl n c3 (CHead e0 (Bind b) w)))))) (\lambda (_: 
+B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) 
+u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: 
+C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) 
+(\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 
+(CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: 
+C).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 e2)))))) (ex4_5 B C C T T 
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda 
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda 
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl 
+n c3 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: 
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) 
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda 
+(_: T).(csubst0 (minus i (S n)) u0 e1 e2))))))) (ty3 g c3 (TLRef n) (lift (S 
+n) O t0)) (\lambda (H8: (getl n c3 (CHead d (Bind Abbr) u))).(ty3_abbr g n c3 
+d u H8 t0 H1)) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: 
+C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 
+(Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda 
+(w: T).(getl n c3 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: 
 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 
 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: 
 T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) 
@@ -132,30 +131,29 @@ T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w))))) (ty3 g c3 (TLRef n)
 T).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 
 (Bind x0) x2))).(\lambda (H10: (getl n c3 (CHead x1 (Bind x0) x3))).(\lambda 
 (H11: (subst0 (minus i (S n)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda 
-(e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow 
-d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind 
-x0) x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C 
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead 
-x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match 
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ 
-t3) \Rightarrow t3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in 
-(\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def 
-(eq_ind_r T x2 (\lambda (t3: T).(subst0 (minus i (S n)) u0 t3 x3)) H11 u H14) 
-in (let H18 \def (eq_ind_r C x1 (\lambda (c0: C).(getl n c3 (CHead c0 (Bind 
-x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl n 
-c3 (CHead d (Bind b) x3))) H18 Abbr H15) in (let H20 \def (eq_ind nat (minus 
-i n) (\lambda (n0: nat).(getl n0 (CHead d (Bind Abbr) x3) (CHead e (Bind 
-Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i 
-(le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead d (Bind Abbr) x3) n 
-H19 (le_S_n n i (le_S (S n) i H6))) (S (minus i (S n))) (minus_x_Sy i n H6)) 
-in (ty3_abbr g n c3 d x3 H19 t0 (H2 (minus i (S n)) u0 d x3 (fsubst0_snd 
-(minus i (S n)) u0 d u x3 H17) e (getl_gen_S (Bind Abbr) d (CHead e (Bind 
-Abbr) u0) x3 (minus i (S n)) H20)))))))))) H13)) H12))))))))) H8)) (\lambda 
-(H8: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda 
-(u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda 
-(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 (CHead e2 
+(e0: C).(match e0 with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow 
+c0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in ((let H13 \def 
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr | 
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _) 
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in 
+((let H14 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) (CHead d (Bind Abbr) u) 
+(CHead x1 (Bind x0) x2) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: 
+(eq C d x1)).(let H17 \def (eq_ind_r T x2 (\lambda (t3: T).(subst0 (minus i 
+(S n)) u0 t3 x3)) H11 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c0: 
+C).(getl n c3 (CHead c0 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r 
+B x0 (\lambda (b: B).(getl n c3 (CHead d (Bind b) x3))) H18 Abbr H15) in (let 
+H20 \def (eq_ind nat (minus i n) (\lambda (n0: nat).(getl n0 (CHead d (Bind 
+Abbr) x3) (CHead e (Bind Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) 
+c3 (csubst0_getl_ge i i (le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) 
+(CHead d (Bind Abbr) x3) n H19 (le_S_n n i (le_S_n (S n) (S i) (le_S (S (S 
+n)) (S i) (le_n_S (S n) i H6))))) (S (minus i (S n))) (minus_x_Sy i n H6)) in 
+(ty3_abbr g n c3 d x3 H19 t0 (H2 (minus i (S n)) u0 d x3 (fsubst0_snd (minus 
+i (S n)) u0 d u x3 H17) e (getl_gen_S (Bind Abbr) d (CHead e (Bind Abbr) u0) 
+x3 (minus i (S n)) H20)))))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4 
+B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq 
+C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: 
+B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 (CHead e2 
 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda 
 (_: T).(csubst0 (minus i (S n)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda 
 (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind 
@@ -166,25 +164,24 @@ u0 e1 e2))))) (ty3 g c3 (TLRef n) (lift (S n) O t0)) (\lambda (x0:
 B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H9: (eq C 
 (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3))).(\lambda (H10: (getl n c3 
 (CHead x2 (Bind x0) x3))).(\lambda (H11: (csubst0 (minus i (S n)) u0 x1 
-x2)).(let H12 \def (f_equal C C (\lambda (e0: C).(match e0 in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow 
-c0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def 
-(f_equal C B (\lambda (e0: C).(match e0 in C return (\lambda (_: C).B) with 
-[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k in K return 
-(\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
-Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H14 
-\def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) 
-with [(CSort _) \Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) (CHead d 
-(Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in (\lambda (H15: (eq B Abbr 
-x0)).(\lambda (H16: (eq C d x1)).(let H17 \def (eq_ind_r T x3 (\lambda (t3: 
-T).(getl n c3 (CHead x2 (Bind x0) t3))) H10 u H14) in (let H18 \def (eq_ind_r 
-C x1 (\lambda (c0: C).(csubst0 (minus i (S n)) u0 c0 x2)) H11 d H16) in (let 
-H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 (CHead x2 (Bind b) u))) 
-H17 Abbr H15) in (let H20 \def (eq_ind nat (minus i n) (\lambda (n0: 
-nat).(getl n0 (CHead x2 (Bind Abbr) u) (CHead e (Bind Abbr) u0))) 
-(getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i (le_n i) c 
-c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead x2 (Bind Abbr) u) n H19 (le_S_n 
-n i (le_S (S n) i H6))) (S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_abbr 
+x2)).(let H12 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) 
+(CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda (e0: 
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead 
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T 
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t3) 
+\Rightarrow t3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in 
+(\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def 
+(eq_ind_r T x3 (\lambda (t3: T).(getl n c3 (CHead x2 (Bind x0) t3))) H10 u 
+H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i (S 
+n)) u0 c0 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: 
+B).(getl n c3 (CHead x2 (Bind b) u))) H17 Abbr H15) in (let H20 \def (eq_ind 
+nat (minus i n) (\lambda (n0: nat).(getl n0 (CHead x2 (Bind Abbr) u) (CHead e 
+(Bind Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 
+(csubst0_getl_ge i i (le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead 
+x2 (Bind Abbr) u) n H19 (le_S_n n i (le_S_n (S n) (S i) (le_S (S (S n)) (S i) 
+(le_n_S (S n) i H6))))) (S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_abbr 
 g n c3 x2 u H19 t0 (H2 (minus i (S n)) u0 x2 u (fsubst0_fst (minus i (S n)) 
 u0 d u x2 H18) e (csubst0_getl_ge_back (minus i (S n)) (minus i (S n)) (le_n 
 (minus i (S n))) d x2 u0 H18 (CHead e (Bind Abbr) u0) (getl_gen_S (Bind Abbr) 
@@ -208,47 +205,45 @@ B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
 (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) 
 x3))).(\lambda (H10: (getl n c3 (CHead x2 (Bind x0) x4))).(\lambda (H11: 
 (subst0 (minus i (S n)) u0 x3 x4)).(\lambda (H12: (csubst0 (minus i (S n)) u0 
-x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow 
-c0])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def 
-(f_equal C B (\lambda (e0: C).(match e0 in C return (\lambda (_: C).B) with 
-[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k in K return 
-(\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
-Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H15 
-\def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) 
-with [(CSort _) \Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) (CHead d 
-(Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in (\lambda (H16: (eq B Abbr 
-x0)).(\lambda (H17: (eq C d x1)).(let H18 \def (eq_ind_r T x3 (\lambda (t3: 
-T).(subst0 (minus i (S n)) u0 t3 x4)) H11 u H15) in (let H19 \def (eq_ind_r C 
-x1 (\lambda (c0: C).(csubst0 (minus i (S n)) u0 c0 x2)) H12 d H17) in (let 
-H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 (CHead x2 (Bind b) x4))) 
-H10 Abbr H16) in (let H21 \def (eq_ind nat (minus i n) (\lambda (n0: 
-nat).(getl n0 (CHead x2 (Bind Abbr) x4) (CHead e (Bind Abbr) u0))) 
-(getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i (le_n i) c 
-c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead x2 (Bind Abbr) x4) n H20 (le_S_n 
-n i (le_S (S n) i H6))) (S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_abbr 
-g n c3 x2 x4 H20 t0 (H2 (minus i (S n)) u0 x2 x4 (fsubst0_both (minus i (S 
-n)) u0 d u x4 H18 x2 H19) e (csubst0_getl_ge_back (minus i (S n)) (minus i (S 
-n)) (le_n (minus i (S n))) d x2 u0 H19 (CHead e (Bind Abbr) u0) (getl_gen_S 
-(Bind Abbr) x2 (CHead e (Bind Abbr) u0) x4 (minus i (S n)) H21))))))))))) 
-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))).(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: 
-nat).(getl n0 c (CHead e (Bind Abbr) u0))) H6 n H7) in (let H10 \def 
-(eq_ind_r nat i (\lambda (n0: nat).(csubst0 n0 u0 c c3)) H5 n H7) in (let H11 
-\def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0: C).(getl n c c0)) H0 
+x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) 
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: 
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead 
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T 
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t3) 
+\Rightarrow t3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in 
+(\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def 
+(eq_ind_r T x3 (\lambda (t3: T).(subst0 (minus i (S n)) u0 t3 x4)) H11 u H15) 
+in (let H19 \def (eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i (S n)) u0 
+c0 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 
+(CHead x2 (Bind b) x4))) H10 Abbr H16) in (let H21 \def (eq_ind nat (minus i 
+n) (\lambda (n0: nat).(getl n0 (CHead x2 (Bind Abbr) x4) (CHead e (Bind Abbr) 
+u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i (le_n 
+i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead x2 (Bind Abbr) x4) n H20 
+(le_S_n n i (le_S_n (S n) (S i) (le_S (S (S n)) (S i) (le_n_S (S n) i H6))))) 
+(S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_abbr g n c3 x2 x4 H20 t0 (H2 
+(minus i (S n)) u0 x2 x4 (fsubst0_both (minus i (S n)) u0 d u x4 H18 x2 H19) 
+e (csubst0_getl_ge_back (minus i (S n)) (minus i (S n)) (le_n (minus i (S 
+n))) d x2 u0 H19 (CHead e (Bind Abbr) u0) (getl_gen_S (Bind Abbr) x2 (CHead e 
+(Bind Abbr) u0) x4 (minus i (S n)) H21))))))))))) 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))).(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: nat).(getl n0 c (CHead e 
+(Bind Abbr) u0))) H6 n H7) in (let H10 \def (eq_ind_r nat i (\lambda (n0: 
+nat).(csubst0 n0 u0 c c3)) H5 n H7) in (let H11 \def (eq_ind C (CHead d (Bind 
+Abbr) u) (\lambda (c0: C).(getl n c c0)) H0 (CHead e (Bind Abbr) u0) 
+(getl_mono c (CHead d (Bind Abbr) u) n H0 (CHead e (Bind Abbr) u0) H9)) in 
+(let H12 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) 
 (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) n H0 (CHead e 
-(Bind Abbr) u0) H9)) in (let H12 \def (f_equal C C (\lambda (e0: C).(match e0 
-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) 
-\Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0) (getl_mono 
-c (CHead d (Bind Abbr) u) n H0 (CHead e (Bind Abbr) u0) H9)) in ((let H13 
-\def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) 
-with [(CSort _) \Rightarrow u | (CHead _ _ t4) \Rightarrow t4])) (CHead d 
+(Bind Abbr) u0) H9)) in ((let H13 \def (f_equal C T (\lambda (e0: C).(match 
+e0 with [(CSort _) \Rightarrow u | (CHead _ _ t4) \Rightarrow t4])) (CHead d 
 (Bind Abbr) u) (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) 
 n H0 (CHead e (Bind Abbr) u0) H9)) in (\lambda (H14: (eq C d e)).(let H15 
 \def (eq_ind_r C e (\lambda (c0: C).(getl n c (CHead c0 (Bind Abbr) u0))) H11 
@@ -276,186 +271,180 @@ O u))) (let H8 \def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c (CHead e
 (Bind Abbr) u0))) H5 n H6) in (let H9 \def (eq_ind C (CHead d (Bind Abst) u) 
 (\lambda (c0: C).(getl n c c0)) H0 (CHead e (Bind Abbr) u0) (getl_mono c 
 (CHead d (Bind Abst) u) n H0 (CHead e (Bind Abbr) u0) H8)) in (let H10 \def 
-(eq_ind C (CHead d (Bind Abst) u) (\lambda (ee: C).(match ee in C return 
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b) 
-\Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow 
-False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) 
-\Rightarrow False])])) I (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind 
-Abst) u) n H0 (CHead e (Bind Abbr) u0) H8)) in (False_ind (ty3 g c (lift (S 
-n) O u0) (lift (S n) O u)) H10)))) t3 H7))) (subst0_gen_lref u0 t3 i n 
-H4)))))) (\lambda (c3: C).(\lambda (H4: (csubst0 i u0 c c3)).(\lambda (e: 
-C).(\lambda (H5: (getl i c (CHead e (Bind Abbr) u0))).(lt_le_e n i (ty3 g c3 
-(TLRef n) (lift (S n) O u)) (\lambda (H6: (lt n i)).(let H7 \def 
-(csubst0_getl_lt i n H6 c c3 u0 H4 (CHead d (Bind Abst) u) H0) in (or4_ind 
-(getl n c3 (CHead d (Bind Abst) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda 
+(eq_ind C (CHead d (Bind Abst) u) (\lambda (ee: C).(match ee with [(CSort _) 
+\Rightarrow False | (CHead _ k _) \Rightarrow (match k with [(Bind b) 
+\Rightarrow (match b with [Abbr \Rightarrow False | Abst \Rightarrow True | 
+Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead e (Bind 
+Abbr) u0) (getl_mono c (CHead d (Bind Abst) u) n H0 (CHead e (Bind Abbr) u0) 
+H8)) in (False_ind (ty3 g c (lift (S n) O u0) (lift (S n) O u)) H10)))) t3 
+H7))) (subst0_gen_lref u0 t3 i n H4)))))) (\lambda (c3: C).(\lambda (H4: 
+(csubst0 i u0 c c3)).(\lambda (e: C).(\lambda (H5: (getl i c (CHead e (Bind 
+Abbr) u0))).(lt_le_e n i (ty3 g c3 (TLRef n) (lift (S n) O u)) (\lambda (H6: 
+(lt n i)).(let H7 \def (csubst0_getl_lt i n H6 c c3 u0 H4 (CHead d (Bind 
+Abst) u) H0) in (or4_ind (getl n c3 (CHead d (Bind Abst) u)) (ex3_4 B C T T 
+(\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C 
+(CHead d (Bind Abst) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda 
+(e0: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 (CHead e0 (Bind b) w)))))) 
+(\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 
+(minus i (S n)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: 
+C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abst) u) (CHead e1 
+(Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda 
+(u1: T).(getl n c3 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: 
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 e2)))))) 
+(ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda 
+(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) 
+u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: 
+T).(\lambda (w: T).(getl n c3 (CHead e2 (Bind b) w))))))) (\lambda (_: 
+B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 
+(minus i (S n)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: 
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 e2))))))) 
+(ty3 g c3 (TLRef n) (lift (S n) O u)) (\lambda (H8: (getl n c3 (CHead d (Bind 
+Abst) u))).(ty3_abst g n c3 d u H8 t0 H1)) (\lambda (H8: (ex3_4 B C T T 
+(\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C 
+(CHead d (Bind Abst) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda 
+(e0: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 (CHead e0 (Bind b) w)))))) 
+(\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 
+(minus i (S n)) u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda 
 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abst) u) (CHead 
 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: 
 T).(\lambda (w: T).(getl n c3 (CHead e0 (Bind b) w)))))) (\lambda (_: 
 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) 
-u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: 
+u0 u1 w))))) (ty3 g c3 (TLRef n) (lift (S n) O u)) (\lambda (x0: B).(\lambda 
+(x1: C).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind 
+Abst) u) (CHead x1 (Bind x0) x2))).(\lambda (H10: (getl n c3 (CHead x1 (Bind 
+x0) x3))).(\lambda (H11: (subst0 (minus i (S n)) u0 x2 x3)).(let H12 \def 
+(f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d | 
+(CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) 
+x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 with 
+[(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with [(Bind 
+b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead d (Bind Abst) u) 
+(CHead x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: 
+C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) 
+(CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2) H9) in (\lambda (H15: (eq B 
+Abst x0)).(\lambda (H16: (eq C d x1)).(let H17 \def (eq_ind_r T x2 (\lambda 
+(t3: T).(subst0 (minus i (S n)) u0 t3 x3)) H11 u H14) in (let H18 \def 
+(eq_ind_r C x1 (\lambda (c0: C).(getl n c3 (CHead c0 (Bind x0) x3))) H10 d 
+H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 (CHead d 
+(Bind b) x3))) H18 Abst H15) in (let H20 \def (eq_ind nat (minus i n) 
+(\lambda (n0: nat).(getl n0 (CHead d (Bind Abst) x3) (CHead e (Bind Abbr) 
+u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i (le_n 
+i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead d (Bind Abst) x3) n H19 
+(le_S_n n i (le_S_n (S n) (S i) (le_S (S (S n)) (S i) (le_n_S (S n) i H6))))) 
+(S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_conv g c3 (lift (S n) O u) 
+(lift (S n) O t0) (ty3_lift g d u t0 H1 c3 O (S n) (getl_drop Abst c3 d x3 n 
+H19)) (TLRef n) (lift (S n) O x3) (ty3_abst g n c3 d x3 H19 t0 (H2 (minus i 
+(S n)) u0 d x3 (fsubst0_snd (minus i (S n)) u0 d u x3 H17) e (getl_gen_S 
+(Bind Abst) d (CHead e (Bind Abbr) u0) x3 (minus i (S n)) H20))) (pc3_lift c3 
+d (S n) O (getl_drop Abst c3 d x3 n H19) x3 u (pc3_pr2_x d x3 u (pr2_delta d 
+e u0 (r (Bind Abst) (minus i (S n))) (getl_gen_S (Bind Abst) d (CHead e (Bind 
+Abbr) u0) x3 (minus i (S n)) H20) u u (pr0_refl u) x3 H17))))))))))) H13)) 
+H12))))))))) H8)) (\lambda (H8: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: 
+C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abst) u) (CHead e1 
+(Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda 
+(u1: T).(getl n c3 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: 
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 
+e2))))))).(ex3_4_ind B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: 
 C).(\lambda (u1: T).(eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1)))))) 
 (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 
 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: 
-C).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 e2)))))) (ex4_5 B C C T T 
-(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda 
-(_: T).(eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1))))))) (\lambda 
-(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl 
-n c3 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: 
-C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) 
-(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda 
-(_: T).(csubst0 (minus i (S n)) u0 e1 e2))))))) (ty3 g c3 (TLRef n) (lift (S 
-n) O u)) (\lambda (H8: (getl n c3 (CHead d (Bind Abst) u))).(ty3_abst g n c3 
-d u H8 t0 H1)) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: 
-C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abst) u) (CHead e0 
-(Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda 
-(w: T).(getl n c3 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: 
-C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 
-w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: 
-T).(\lambda (_: T).(eq C (CHead d (Bind Abst) u) (CHead e0 (Bind b) u1)))))) 
-(\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 
-(CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: C).(\lambda (u1: 
-T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w))))) (ty3 g c3 (TLRef n) 
-(lift (S n) O u)) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda 
+C).(\lambda (_: T).(csubst0 (minus i (S n)) u0 e1 e2))))) (ty3 g c3 (TLRef n) 
+(lift (S n) O u)) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda 
 (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) 
-x2))).(\lambda (H10: (getl n c3 (CHead x1 (Bind x0) x3))).(\lambda (H11: 
-(subst0 (minus i (S n)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0: 
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | 
-(CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) 
-x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C return 
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b) 
-\Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead d (Bind Abst) u) (CHead 
-x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match 
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ 
-t3) \Rightarrow t3])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x2) H9) in 
-(\lambda (H15: (eq B Abst x0)).(\lambda (H16: (eq C d x1)).(let H17 \def 
-(eq_ind_r T x2 (\lambda (t3: T).(subst0 (minus i (S n)) u0 t3 x3)) H11 u H14) 
-in (let H18 \def (eq_ind_r C x1 (\lambda (c0: C).(getl n c3 (CHead c0 (Bind 
-x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: B).(getl n 
-c3 (CHead d (Bind b) x3))) H18 Abst H15) in (let H20 \def (eq_ind nat (minus 
-i n) (\lambda (n0: nat).(getl n0 (CHead d (Bind Abst) x3) (CHead e (Bind 
-Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i 
-(le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead d (Bind Abst) x3) n 
-H19 (le_S_n n i (le_S (S n) i H6))) (S (minus i (S n))) (minus_x_Sy i n H6)) 
-in (ty3_conv g c3 (lift (S n) O u) (lift (S n) O t0) (ty3_lift g d u t0 H1 c3 
-O (S n) (getl_drop Abst c3 d x3 n H19)) (TLRef n) (lift (S n) O x3) (ty3_abst 
-g n c3 d x3 H19 t0 (H2 (minus i (S n)) u0 d x3 (fsubst0_snd (minus i (S n)) 
-u0 d u x3 H17) e (getl_gen_S (Bind Abst) d (CHead e (Bind Abbr) u0) x3 (minus 
-i (S n)) H20))) (pc3_lift c3 d (S n) O (getl_drop Abst c3 d x3 n H19) x3 u 
-(pc3_pr2_x d x3 u (pr2_delta d e u0 (r (Bind Abst) (minus i (S n))) 
-(getl_gen_S (Bind Abst) d (CHead e (Bind Abbr) u0) x3 (minus i (S n)) H20) u 
-u (pr0_refl u) x3 H17))))))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4 
-B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq 
-C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: 
-B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl n c3 (CHead e2 
-(Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda 
-(_: T).(csubst0 (minus i (S n)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda 
-(b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind 
-Abst) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda 
-(e2: C).(\lambda (u1: T).(getl n c3 (CHead e2 (Bind b) u1)))))) (\lambda (_: 
-B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i (S n)) 
-u0 e1 e2))))) (ty3 g c3 (TLRef n) (lift (S n) O u)) (\lambda (x0: B).(\lambda 
-(x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind 
-Abst) u) (CHead x1 (Bind x0) x3))).(\lambda (H10: (getl n c3 (CHead x2 (Bind 
-x0) x3))).(\lambda (H11: (csubst0 (minus i (S n)) u0 x1 x2)).(let H12 \def 
-(f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with 
-[(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind 
-Abst) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda 
-(e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow 
-Abst | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with 
-[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead d (Bind Abst) 
-u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0: 
-C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | 
-(CHead _ _ t3) \Rightarrow t3])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) 
-x3) H9) in (\lambda (H15: (eq B Abst x0)).(\lambda (H16: (eq C d x1)).(let 
-H17 \def (eq_ind_r T x3 (\lambda (t3: T).(getl n c3 (CHead x2 (Bind x0) t3))) 
-H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i 
-(S n)) u0 c0 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b: 
-B).(getl n c3 (CHead x2 (Bind b) u))) H17 Abst H15) in (let H20 \def (eq_ind 
-nat (minus i n) (\lambda (n0: nat).(getl n0 (CHead x2 (Bind Abst) u) (CHead e 
-(Bind Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 
-(csubst0_getl_ge i i (le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead 
-x2 (Bind Abst) u) n H19 (le_S_n n i (le_S (S n) i H6))) (S (minus i (S n))) 
-(minus_x_Sy i n H6)) in (ty3_abst g n c3 x2 u H19 t0 (H2 (minus i (S n)) u0 
-x2 u (fsubst0_fst (minus i (S n)) u0 d u x2 H18) e (csubst0_getl_ge_back 
-(minus i (S n)) (minus i (S n)) (le_n (minus i (S n))) d x2 u0 H18 (CHead e 
-(Bind Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e (Bind Abbr) u0) u (minus 
-i (S n)) H20))))))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex4_5 B C C T 
-T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda 
-(_: T).(eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1))))))) (\lambda 
-(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl 
-n c3 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: 
-C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) 
-(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda 
-(_: T).(csubst0 (minus i (S n)) u0 e1 e2)))))))).(ex4_5_ind B C C T T 
-(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda 
-(_: T).(eq C (CHead d (Bind Abst) u) (CHead e1 (Bind b) u1))))))) (\lambda 
-(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl 
-n c3 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: 
-C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) 
-(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda 
-(_: T).(csubst0 (minus i (S n)) u0 e1 e2)))))) (ty3 g c3 (TLRef n) (lift (S 
-n) O u)) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: 
-T).(\lambda (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abst) u) (CHead x1 
-(Bind x0) x3))).(\lambda (H10: (getl n c3 (CHead x2 (Bind x0) x4))).(\lambda 
-(H11: (subst0 (minus i (S n)) u0 x3 x4)).(\lambda (H12: (csubst0 (minus i (S 
-n)) u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 in C 
-return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) 
-\Rightarrow c0])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in 
-((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C return (\lambda 
-(_: C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match 
-k in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) 
+x3))).(\lambda (H10: (getl n c3 (CHead x2 (Bind x0) x3))).(\lambda (H11: 
+(csubst0 (minus i (S n)) u0 x1 x2)).(let H12 \def (f_equal C C (\lambda (e0: 
+C).(match e0 with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) 
+(CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def 
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abst | 
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _) 
 \Rightarrow Abst])])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in 
-((let H15 \def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda 
-(_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) 
-(CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in (\lambda (H16: (eq B 
-Abst x0)).(\lambda (H17: (eq C d x1)).(let H18 \def (eq_ind_r T x3 (\lambda 
-(t3: T).(subst0 (minus i (S n)) u0 t3 x4)) H11 u H15) in (let H19 \def 
-(eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i (S n)) u0 c0 x2)) H12 d 
-H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 (CHead x2 
-(Bind b) x4))) H10 Abst H16) in (let H21 \def (eq_ind nat (minus i n) 
-(\lambda (n0: nat).(getl n0 (CHead x2 (Bind Abst) x4) (CHead e (Bind Abbr) 
+((let H14 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow u | (CHead _ _ t3) \Rightarrow t3])) (CHead d (Bind Abst) u) 
+(CHead x1 (Bind x0) x3) H9) in (\lambda (H15: (eq B Abst x0)).(\lambda (H16: 
+(eq C d x1)).(let H17 \def (eq_ind_r T x3 (\lambda (t3: T).(getl n c3 (CHead 
+x2 (Bind x0) t3))) H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c0: 
+C).(csubst0 (minus i (S n)) u0 c0 x2)) H11 d H16) in (let H19 \def (eq_ind_r 
+B x0 (\lambda (b: B).(getl n c3 (CHead x2 (Bind b) u))) H17 Abst H15) in (let 
+H20 \def (eq_ind nat (minus i n) (\lambda (n0: nat).(getl n0 (CHead x2 (Bind 
+Abst) u) (CHead e (Bind Abbr) u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) 
+c3 (csubst0_getl_ge i i (le_n i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) 
+(CHead x2 (Bind Abst) u) n H19 (le_S_n n i (le_S_n (S n) (S i) (le_S (S (S 
+n)) (S i) (le_n_S (S n) i H6))))) (S (minus i (S n))) (minus_x_Sy i n H6)) in 
+(ty3_abst g n c3 x2 u H19 t0 (H2 (minus i (S n)) u0 x2 u (fsubst0_fst (minus 
+i (S n)) u0 d u x2 H18) e (csubst0_getl_ge_back (minus i (S n)) (minus i (S 
+n)) (le_n (minus i (S n))) d x2 u0 H18 (CHead e (Bind Abbr) u0) (getl_gen_S 
+(Bind Abst) x2 (CHead e (Bind Abbr) u0) u (minus i (S n)) H20))))))))))) 
+H13)) H12))))))))) H8)) (\lambda (H8: (ex4_5 B C C T T (\lambda (b: 
+B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(eq C 
+(CHead d (Bind Abst) u) (CHead e1 (Bind b) u1))))))) (\lambda (b: B).(\lambda 
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 (CHead e2 
+(Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: C).(\lambda 
+(u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) (\lambda (_: 
+B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 
+(minus i (S n)) u0 e1 e2)))))))).(ex4_5_ind B C C T T (\lambda (b: 
+B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(eq C 
+(CHead d (Bind Abst) u) (CHead e1 (Bind b) u1))))))) (\lambda (b: B).(\lambda 
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl n c3 (CHead e2 
+(Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: C).(\lambda 
+(u1: T).(\lambda (w: T).(subst0 (minus i (S n)) u0 u1 w)))))) (\lambda (_: 
+B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 
+(minus i (S n)) u0 e1 e2)))))) (ty3 g c3 (TLRef n) (lift (S n) O u)) (\lambda 
+(x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: 
+T).(\lambda (H9: (eq C (CHead d (Bind Abst) u) (CHead x1 (Bind x0) 
+x3))).(\lambda (H10: (getl n c3 (CHead x2 (Bind x0) x4))).(\lambda (H11: 
+(subst0 (minus i (S n)) u0 x3 x4)).(\lambda (H12: (csubst0 (minus i (S n)) u0 
+x1 x2)).(let H13 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abst) u) 
+(CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: 
+C).(match e0 with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead 
+d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T 
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t3) 
+\Rightarrow t3])) (CHead d (Bind Abst) u) (CHead x1 (Bind x0) x3) H9) in 
+(\lambda (H16: (eq B Abst x0)).(\lambda (H17: (eq C d x1)).(let H18 \def 
+(eq_ind_r T x3 (\lambda (t3: T).(subst0 (minus i (S n)) u0 t3 x4)) H11 u H15) 
+in (let H19 \def (eq_ind_r C x1 (\lambda (c0: C).(csubst0 (minus i (S n)) u0 
+c0 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl n c3 
+(CHead x2 (Bind b) x4))) H10 Abst H16) in (let H21 \def (eq_ind nat (minus i 
+n) (\lambda (n0: nat).(getl n0 (CHead x2 (Bind Abst) x4) (CHead e (Bind Abbr) 
 u0))) (getl_conf_le i (CHead e (Bind Abbr) u0) c3 (csubst0_getl_ge i i (le_n 
 i) c c3 u0 H4 (CHead e (Bind Abbr) u0) H5) (CHead x2 (Bind Abst) x4) n H20 
-(le_S_n n i (le_S (S n) i H6))) (S (minus i (S n))) (minus_x_Sy i n H6)) in 
-(ty3_conv g c3 (lift (S n) O u) (lift (S n) O t0) (ty3_lift g x2 u t0 (H2 
-(minus i (S n)) u0 x2 u (fsubst0_fst (minus i (S n)) u0 d u x2 H19) e 
-(csubst0_getl_ge_back (minus i (S n)) (minus i (S n)) (le_n (minus i (S n))) 
-d x2 u0 H19 (CHead e (Bind Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e 
-(Bind Abbr) u0) x4 (minus i (S n)) H21))) c3 O (S n) (getl_drop Abst c3 x2 x4 
-n H20)) (TLRef n) (lift (S n) O x4) (ty3_abst g n c3 x2 x4 H20 t0 (H2 (minus 
-i (S n)) u0 x2 x4 (fsubst0_both (minus i (S n)) u0 d u x4 H18 x2 H19) e 
-(csubst0_getl_ge_back (minus i (S n)) (minus i (S n)) (le_n (minus i (S n))) 
-d x2 u0 H19 (CHead e (Bind Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e 
-(Bind Abbr) u0) x4 (minus i (S n)) H21)))) (pc3_lift c3 x2 (S n) O (getl_drop 
-Abst c3 x2 x4 n H20) x4 u (pc3_fsubst0 d u u (pc3_refl d u) (minus i (S n)) 
-u0 x2 x4 (fsubst0_both (minus i (S n)) u0 d u x4 H18 x2 H19) e 
-(csubst0_getl_ge_back (minus i (S n)) (minus i (S n)) (le_n (minus i (S n))) 
-d x2 u0 H19 (CHead e (Bind Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e 
-(Bind Abbr) u0) x4 (minus i (S n)) H21)))))))))))) H14)) H13))))))))))) H8)) 
-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))).(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: 
-nat).(csubst0 n0 u0 c c3)) H5 n H7) in (let H11 \def (eq_ind C (CHead d (Bind 
-Abst) u) (\lambda (c0: C).(getl n c c0)) H0 (CHead e (Bind Abbr) u0) 
-(getl_mono c (CHead d (Bind Abst) u) n H0 (CHead e (Bind Abbr) u0) H9)) in 
-(let H12 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda (ee: C).(match ee in 
-C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k 
-_) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b) 
-\Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow 
-False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) 
-\Rightarrow False])])) I (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind 
-Abst) u) n H0 (CHead e (Bind Abbr) u0) H9)) in (False_ind (ty3 g c3 (lift (S 
-n) O u0) (lift (S n) O u)) H12))))) t3 H8))) (subst0_gen_lref u0 t3 i n 
-H4)))))))) c2 t2 H3)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda 
-(t0: T).(\lambda (H0: (ty3 g c u t0)).(\lambda (H1: ((\forall (i: 
+(le_S_n n i (le_S_n (S n) (S i) (le_S (S (S n)) (S i) (le_n_S (S n) i H6))))) 
+(S (minus i (S n))) (minus_x_Sy i n H6)) in (ty3_conv g c3 (lift (S n) O u) 
+(lift (S n) O t0) (ty3_lift g x2 u t0 (H2 (minus i (S n)) u0 x2 u 
+(fsubst0_fst (minus i (S n)) u0 d u x2 H19) e (csubst0_getl_ge_back (minus i 
+(S n)) (minus i (S n)) (le_n (minus i (S n))) d x2 u0 H19 (CHead e (Bind 
+Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e (Bind Abbr) u0) x4 (minus i (S 
+n)) H21))) c3 O (S n) (getl_drop Abst c3 x2 x4 n H20)) (TLRef n) (lift (S n) 
+O x4) (ty3_abst g n c3 x2 x4 H20 t0 (H2 (minus i (S n)) u0 x2 x4 
+(fsubst0_both (minus i (S n)) u0 d u x4 H18 x2 H19) e (csubst0_getl_ge_back 
+(minus i (S n)) (minus i (S n)) (le_n (minus i (S n))) d x2 u0 H19 (CHead e 
+(Bind Abbr) u0) (getl_gen_S (Bind Abst) x2 (CHead e (Bind Abbr) u0) x4 (minus 
+i (S n)) H21)))) (pc3_lift c3 x2 (S n) O (getl_drop Abst c3 x2 x4 n H20) x4 u 
+(pc3_fsubst0 d u u (pc3_refl d u) (minus i (S n)) u0 x2 x4 (fsubst0_both 
+(minus i (S n)) u0 d u x4 H18 x2 H19) e (csubst0_getl_ge_back (minus i (S n)) 
+(minus i (S n)) (le_n (minus i (S n))) d x2 u0 H19 (CHead e (Bind Abbr) u0) 
+(getl_gen_S (Bind Abst) x2 (CHead e (Bind Abbr) u0) x4 (minus i (S n)) 
+H21)))))))))))) H14)) H13))))))))))) H8)) 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))).(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: nat).(csubst0 n0 u0 c c3)) H5 n 
+H7) in (let H11 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda (c0: C).(getl 
+n c c0)) H0 (CHead e (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abst) u) n 
+H0 (CHead e (Bind Abbr) u0) H9)) in (let H12 \def (eq_ind C (CHead d (Bind 
+Abst) u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | 
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with 
+[Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | 
+(Flat _) \Rightarrow False])])) I (CHead e (Bind Abbr) u0) (getl_mono c 
+(CHead d (Bind Abst) u) n H0 (CHead e (Bind Abbr) u0) H9)) in (False_ind (ty3 
+g c3 (lift (S n) O u0) (lift (S n) O u)) H12))))) t3 H8))) (subst0_gen_lref 
+u0 t3 i n 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 (H2: 
@@ -959,11 +948,8 @@ Cast) t0 t3)) i u c3 (THead (Flat Cast) t0 x0) (fsubst0_both i u c (THead
 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))))).
-(* COMMENTS
-Initial nodes: 23439
-END *)
 
-theorem ty3_csubst0:
+lemma ty3_csubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
 t1 t2) \to (\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c1 
 (CHead e (Bind Abbr) u)) \to (\forall (c2: C).((csubst0 i u c1 c2) \to (ty3 g 
@@ -974,11 +960,8 @@ c2 t1 t2)))))))))))
 nat).(\lambda (H0: (getl i c1 (CHead e (Bind Abbr) u))).(\lambda (c2: 
 C).(\lambda (H1: (csubst0 i u c1 c2)).(ty3_fsubst0 g c1 t1 t2 H i u c2 t1 
 (fsubst0_fst i u c1 t1 c2 H1) e H0))))))))))).
-(* COMMENTS
-Initial nodes: 89
-END *)
 
-theorem ty3_subst0:
+lemma ty3_subst0:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((ty3 g c t1 
 t) \to (\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead e 
 (Bind Abbr) u)) \to (\forall (t2: T).((subst0 i u t1 t2) \to (ty3 g c t2 
@@ -989,7 +972,4 @@ t)))))))))))
 (H0: (getl i c (CHead e (Bind Abbr) u))).(\lambda (t2: T).(\lambda (H1: 
 (subst0 i u t1 t2)).(ty3_fsubst0 g c t1 t H i u c t2 (fsubst0_snd i u c t1 t2 
 H1) e H0))))))))))).
-(* COMMENTS
-Initial nodes: 89
-END *)