dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / ex2 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex2/props.ma
index b596f85a2f896c987d390bcd077089f2e3ee2b70..4dfa6a5825e07d9e72bd27dea2c425caf64c00f0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex2/props.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ex2/defs.ma".
+include "Basic-1/ex2/defs.ma".
 
-include "LambdaDelta-1/nf2/defs.ma".
+include "Basic-1/nf2/defs.ma".
 
-include "LambdaDelta-1/pr2/fwd.ma".
+include "Basic-1/pr2/fwd.ma".
 
-include "LambdaDelta-1/arity/fwd.ma".
+include "Basic-1/arity/fwd.ma".
 
 theorem ex2_nf2:
  nf2 ex2_c ex2_t
@@ -130,6 +130,9 @@ t)) (let H9 \def (eq_ind T (TSort O) (\lambda (ee: T).(match ee in T return
 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))).
+(* COMMENTS
+Initial nodes: 1939
+END *)
 
 theorem ex2_arity:
  \forall (g: G).(\forall (a: A).((arity g ex2_c ex2_t a) \to (\forall (P: 
@@ -150,4 +153,7 @@ a4))) (\lambda (a3: A).(\lambda (a4: A).(eq A (ASort O O) (AHead a3 a4)))) P
 (eq_ind A (ASort O O) (\lambda (ee: A).(match ee in A return (\lambda (_: 
 A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow 
 False])) I (AHead x0 x1) H6) in (False_ind P H7))))))) H3)))))) H0))))).
+(* COMMENTS
+Initial nodes: 289
+END *)