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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/getl/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/getl/dec.ma
index dda85e7f3..a8f4df8bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/getl/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/getl/dec.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/getl/props.ma".
 
-theorem getl_dec:
+lemma getl_dec:
  \forall (c: C).(\forall (i: nat).(or (ex_3 C B T (\lambda (e: C).(\lambda 
 (b: B).(\lambda (v: T).(getl i c (CHead e (Bind b) v)))))) (\forall (d: 
 C).((getl i c d) \to (\forall (P: Prop).P)))))