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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/getl/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/getl/getl.ma
index 71327becf..64e331905 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/getl/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/getl/getl.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/getl/drop.ma".
+include "basic_1/getl/drop.ma".
 
-include "Basic-1/getl/clear.ma".
+include "basic_1/getl/clear.ma".
 
-theorem getl_conf_le:
+lemma getl_conf_le:
  \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall 
 (e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e 
 a))))))))
@@ -30,9 +30,6 @@ a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (H0: (getl h c e)).(\lambda
 a) (\lambda (x: C).(\lambda (H3: (drop h O c x)).(\lambda (H4: (clear x 
 e)).(getl_clear_conf (minus i h) x a (getl_drop_conf_ge i a c H x h O H3 H1) 
 e H4)))) H2))))))))).
-(* COMMENTS
-Initial nodes: 133
-END *)
 
 theorem getl_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl 
@@ -51,7 +48,4 @@ h) c1 c2 H e2 H5))) (\lambda (i0: nat).(\lambda (_: (((drop i0 O c2 x) \to
 (getl (plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def 
 (getl_drop_trans c1 c2 h H x i0 H4) in (getl_intro (plus (S i0) h) c1 e2 x 
 H_y H3))))) i H2)))) H1)))))))).
-(* COMMENTS
-Initial nodes: 247
-END *)