X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Flift1.ma;h=71d9e93fe566cef9074b090726d46fea7b999b88;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=24d0f4ed6eb7b30ff35749db451ef4227c3fa49c;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma b/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
index 24d0f4ed6..71d9e93fe 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
@@ -20,7 +20,7 @@ include "basic_1/drop1/fwd.ma".
 
 include "basic_1/lift1/props.ma".
 
-theorem sns3_lifts1:
+lemma sns3_lifts1:
  \forall (e: C).(\forall (hds: PList).(\forall (c: C).((drop1 hds c e) \to 
 (\forall (ts: TList).((sns3 e ts) \to (sns3 c (lifts1 hds ts)))))))
 \def