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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
index 69849f3f1..f75c1c75a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
@@ -18,7 +18,7 @@ include "basic_1/sty0/fwd.ma".
 
 include "basic_1/getl/drop.ma".
 
-theorem sty0_lift:
+lemma sty0_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e 
 t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall (d: nat).((drop h d c 
 e) \to (sty0 g c (lift h d t1) (lift h d t2))))))))))
@@ -163,7 +163,7 @@ h d H4) (lift h (s (Flat Cast) d) t3) (lift h (s (Flat Cast) d) t4) (H3 c0 h
 Cast) v2 t4 h d)) (lift h d (THead (Flat Cast) v1 t3)) (lift_head (Flat Cast) 
 v1 t3 h d))))))))))))))) e t1 t2 H))))).
 
-theorem sty0_correct:
+lemma sty0_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
 t1 t) \to (ex T (\lambda (t2: T).(sty0 g c t t2)))))))
 \def