X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fex1%2Fprops.ma;h=91ce1745bcad69dfb68c1ba063bd5250ac6aa922;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=95b5201a9baadde663e72395ec437708b968c957;hpb=10c836687dfdf9d23357d7423cfc535e817d843f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
index 95b5201a9..91ce1745b 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
@@ -28,14 +28,14 @@ include "basic_1/arity/defs.ma".
 
 include "basic_1/leq/props.ma".
 
-theorem ex1__leq_sort_SS:
+fact ex1__leq_sort_SS:
  \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc 
 g (asucc g (ASort (S (S k)) n))))))
 \def
  \lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g 
 (asucc g (ASort (S (S k)) n)))))).
 
-theorem ex1_arity:
+lemma ex1_arity:
  \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
 \def
  \lambda (g: G).(arity_appl g (CHead (CHead (CHead (CSort O) (Bind Abst) 
@@ -67,7 +67,7 @@ O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
 
-theorem ex1_ty3:
+lemma ex1_ty3:
  \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P: 
 Prop).P)))
 \def