X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fex2%2Fprops.ma;h=42c2de64690174450e8494115675cbb8b967489e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=d5192ec5473c16586b851b8c36781fe3d567c806;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex2/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ex2/props.ma
index d5192ec54..42c2de646 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ex2/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ex2/props.ma
@@ -22,7 +22,7 @@ include "basic_1/pr2/fwd.ma".
 
 include "basic_1/arity/fwd.ma".
 
-theorem ex2_nf2:
+lemma ex2_nf2:
  nf2 ex2_c ex2_t
 \def
  \lambda (t2: T).(\lambda (H: (pr2 (CSort O) (THead (Flat Appl) (TSort O) 
@@ -130,7 +130,7 @@ False])) I (THead (Bind x0) x1 x2) H3) in (False_ind (eq T (THead (Flat Appl)
 (TSort O) (TSort O)) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O 
 (TSort O)) x3))) H9)) t2 H8))))))))))))))) H1)) H0))).
 
-theorem ex2_arity:
+lemma ex2_arity:
  \forall (g: G).(\forall (a: A).((arity g ex2_c ex2_t a) \to (\forall (P: 
 Prop).P)))
 \def