update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / pr0 / dec.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/dec.ma
index 96d70c708f8402008a5027f9e8852946ef4910f4..889e820348c86eb07026deb5c63df2e658ca1e42 100644 (file)
--- 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))))