update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / ex1 / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
index 95b5201a9baadde663e72395ec437708b968c957..91ce1745bcad69dfb68c1ba063bd5250ac6aa922 100644 (file)
--- 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".
 
 
 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)))))).
 
  \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) 
  \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))).
 
 (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
  \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P: 
 Prop).P)))
 \def