X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fex1%2Fprops.ma;h=5c442f5bb431285e31bce298bf2c86601a0dc472;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=9c94c211177c8bcaec4d6b157ba8e6b1f3d24801;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex1/props.ma
index 9c94c2111..5c442f5bb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex1/props.ma
@@ -14,19 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ex1/defs.ma".
+include "Basic-1/ex1/defs.ma".
 
-include "LambdaDelta-1/ty3/fwd.ma".
+include "Basic-1/ty3/fwd.ma".
 
-include "LambdaDelta-1/pc3/fwd.ma".
+include "Basic-1/pc3/fwd.ma".
 
-include "LambdaDelta-1/nf2/pr3.ma".
+include "Basic-1/nf2/pr3.ma".
 
-include "LambdaDelta-1/nf2/props.ma".
+include "Basic-1/nf2/props.ma".
 
-include "LambdaDelta-1/arity/defs.ma".
+include "Basic-1/arity/defs.ma".
 
-include "LambdaDelta-1/leq/props.ma".
+include "Basic-1/leq/props.ma".
 
 theorem ex1__leq_sort_SS:
  \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc 
@@ -34,6 +34,9 @@ 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)))))).
+(* COMMENTS
+Initial nodes: 27
+END *)
 
 theorem ex1_arity:
  \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
@@ -66,6 +69,9 @@ O) (ASort O O) (arity_sort g (CSort O) O) (asucc g (asucc g (ASort (S (S O))
 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))).
+(* COMMENTS
+Initial nodes: 753
+END *)
 
 theorem ex1_ty3:
  \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P: 
@@ -524,4 +530,7 @@ H10)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 (TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead (CHead (CHead (CSort O) 
 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
 O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u H))))).
+(* COMMENTS
+Initial nodes: 9973
+END *)