X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fclen%2Fgetl.ma;h=55bad4ad9fb9f8dc0796ba5fb4517fe87aa27fa5;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=956a7b64e09802a6a69252eda8cfcff38c2aef72;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
index 956a7b64e..55bad4ad9 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
@@ -18,7 +18,7 @@ include "basic_1/clen/defs.ma".
 
 include "basic_1/getl/props.ma".
 
-theorem getl_ctail_clen:
+lemma getl_ctail_clen:
  \forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n: 
 nat).(getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t))))))
 \def
@@ -42,7 +42,7 @@ F).(ex_intro nat (\lambda (n: nat).(getl (clen c0) (CHead (CTail (Bind b) t
 c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x (getl_flat (CTail (Bind b) 
 t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f t0))) k))) H0)))))) c))).
 
-theorem getl_gen_tail:
+lemma getl_gen_tail:
  \forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall 
 (c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2 
 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))