X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr0%2Fdec.ma;h=889e820348c86eb07026deb5c63df2e658ca1e42;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=96d70c708f8402008a5027f9e8852946ef4910f4;hpb=5ff05b234ea985b91bfe6ef3e8dd54eeeb477e11;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma
index 96d70c708..889e82034 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma
@@ -22,7 +22,7 @@ include "basic_1/T/dec.ma".
 
 include "basic_1/T/props.ma".
 
-theorem nf0_dec:
+lemma nf0_dec:
  \forall (t1: T).(or (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T 
 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: 
 T).(pr0 t1 t2))))