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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubt/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/csubt/getl.ma
index df14528ed..7156f6296 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubt/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubt/getl.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/csubt/clear.ma".
+include "basic_1/csubt/clear.ma".
 
-include "Basic-1/csubt/drop.ma".
+include "basic_1/csubt/drop.ma".
 
-include "Basic-1/getl/clear.ma".
+include "basic_1/getl/clear.ma".
 
-theorem csubt_getl_abbr:
+lemma csubt_getl_abbr:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall 
 (n: nat).((getl n c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csubt g 
 c1 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n 
@@ -50,24 +50,22 @@ u))).(K_ind (\lambda (k0: K).((drop n O c1 (CHead x0 k0 t)) \to ((clear
 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 
 (CHead d2 (Bind Abbr) u))))))))) (\lambda (b: B).(\lambda (H5: (drop n O c1 
 (CHead x0 (Bind b) t))).(\lambda (H6: (clear (CHead x0 (Bind b) t) (CHead d1 
-(Bind Abbr) u))).(let H7 \def (f_equal C C (\lambda (e: C).(match e in C 
-return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _) 
-\Rightarrow c])) (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t) 
-(clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in ((let H8 \def 
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with 
-[(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 in K 
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) 
-\Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t) 
-(clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in ((let H9 \def 
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with 
-[(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind 
+(Bind Abbr) u))).(let H7 \def (f_equal C C (\lambda (e: C).(match e with 
+[(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind 
 Abbr) u) (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) 
-t H6)) in (\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda 
-(c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda 
-(t0: T).(drop n O c1 (CHead x0 (Bind b) t0))) H5 u H9) in (let H14 \def 
-(eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) u))) H13 Abbr 
-H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1 (CHead c 
-(Bind Abbr) u))) H14 d1 H11) in (ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) 
+t H6)) in ((let H8 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0) 
+\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u) 
+(CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in 
+((let H9 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abbr) u) 
+(CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in 
+(\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2: 
+C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda (t0: 
+T).(drop n O c1 (CHead x0 (Bind b) t0))) H5 u H9) in (let H14 \def (eq_ind_r 
+B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) u))) H13 Abbr H10) in 
+(let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1 (CHead c (Bind 
+Abbr) u))) H14 d1 H11) in (ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) 
 (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abbr) u))) (ex2 C (\lambda (d2: 
 C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u)))) 
 (\lambda (x1: C).(\lambda (H16: (csubt g d1 x1)).(\lambda (H17: (drop n O c2 
@@ -135,11 +133,8 @@ d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr) u))) x9 H22
 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) u) n0 H23))))) 
 H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))) k H3 H4))))))) x H1 
 H2)))) H0))))))).
-(* COMMENTS
-Initial nodes: 2313
-END *)
 
-theorem csubt_getl_abst:
+lemma csubt_getl_abst:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (t: T).(\forall 
 (n: nat).((getl n c1 (CHead d1 (Bind Abst) t)) \to (\forall (c2: C).((csubt g 
 c1 c2) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: 
@@ -189,52 +184,51 @@ T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n c2 (CHead d2
 (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (b: B).(\lambda (H5: 
 (drop n O c1 (CHead x0 (Bind b) t0))).(\lambda (H6: (clear (CHead x0 (Bind b) 
 t0) (CHead d1 (Bind Abst) t))).(let H7 \def (f_equal C C (\lambda (e: 
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | 
-(CHead c _ _) \Rightarrow c])) (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) 
-t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H8 \def 
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with 
-[(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 in K 
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) 
-\Rightarrow Abst])])) (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) 
-(clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H9 \def 
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with 
-[(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1])) (CHead d1 (Bind 
-Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t) 
-t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1 
-x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r 
-T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t H9) in (let 
-H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) t))) 
-H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1 
-(CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C (\lambda (d2: 
-C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t)))) 
-(ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: 
-C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: 
-C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g 
-d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: 
-C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: 
-C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n 
-c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u 
-t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H16: (ex2 
-C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 
-(Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: 
-C).(drop n O c2 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt 
-g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T 
-(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda 
-(u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: 
-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) 
-(\lambda (x1: C).(\lambda (H17: (csubt g d1 x1)).(\lambda (H18: (drop n O c2 
-(CHead x1 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 
+C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) 
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead 
+d1 (Bind Abst) t) t0 H6)) in ((let H8 \def (f_equal C B (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow 
+(match k0 with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) 
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead 
+d1 (Bind Abst) t) t0 H6)) in ((let H9 \def (f_equal C T (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1])) 
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead 
+d1 (Bind Abst) t) t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq 
+C d1 x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def 
+(eq_ind_r T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t 
+H9) in (let H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 
+(Bind b0) t))) H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: 
+C).(drop n O c1 (CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C 
+(\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 
+(Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) 
+u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: 
+C).(\lambda (u: T).(ty3 g d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 
 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T 
 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda 
 (u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: 
-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) 
-(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 
-(CHead d2 (Bind Abst) t))) x1 H17 (getl_intro n c2 (CHead x1 (Bind Abst) t) 
-(CHead x1 (Bind Abst) t) H18 (clear_bind Abst x1 t))))))) H16)) (\lambda 
-(H16: (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda 
-(d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: 
-C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g 
-d2 u t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) 
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) 
+(\lambda (H16: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: 
+C).(drop n O c2 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: 
+C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t))) 
+(or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 
+(CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: 
+T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n c2 (CHead d2 
+(Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda 
+(d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x1: C).(\lambda (H17: 
+(csubt g d1 x1)).(\lambda (H18: (drop n O c2 (CHead x1 (Bind Abst) 
+t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: 
+C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: 
+C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n 
+c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u 
+t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda 
+(d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) 
+t))) x1 H17 (getl_intro n c2 (CHead x1 (Bind Abst) t) (CHead x1 (Bind Abst) 
+t) H18 (clear_bind Abst x1 t))))))) H16)) (\lambda (H16: (ex4_2 C T (\lambda 
+(d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: 
+T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: 
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u 
+t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) 
 (\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) 
 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda 
 (u: T).(ty3 g d2 u t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda 
@@ -420,7 +414,4 @@ x7 (CHead x9 (Bind Abbr) x10))).(\lambda (H25: (ty3 g d1 x10 t)).(\lambda
 g d2 u t))) x9 x10 H23 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) 
 x10) n0 H24) H25 H26)))))))) H22)) H21)))))))) H17))))) H14))))))) 
 H11)))))))) n) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
-(* COMMENTS
-Initial nodes: 5861
-END *)