X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsubst0%2Fdec.ma;h=93aa0736a340c2d11a253bf2d86a051a4c5be284;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=4a70958c1142832dbce0724de7611e29405fd2ba;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
index 4a70958c1..93aa0736a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
@@ -18,7 +18,7 @@ include "basic_1/subst0/defs.ma".
 
 include "basic_1/lift/props.ma".
 
-theorem dnf_dec2:
+lemma dnf_dec2:
  \forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: 
 T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S 
 O) d v))))))
@@ -148,7 +148,7 @@ x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(eq T (THead k (lift (S O) d x)
 (S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) 
 d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).
 
-theorem dnf_dec:
+lemma dnf_dec:
  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or 
 (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))
 \def