uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / wf3 / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/fwd.ma
index aa63ef78a46e82cb0b81f126176a134e4bd7cdc7..71c903f0641518006bd77aa72b668fa03d9f7955 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wf3/defs.ma".
+include "Basic-1/wf3/defs.ma".
 
 theorem wf3_gen_sort1:
  \forall (g: G).(\forall (x: C).(\forall (m: nat).((wf3 g (CSort m) x) \to 
@@ -49,6 +49,9 @@ f) u) (CSort m))).(let H4 \def (eq_ind C (CHead c1 (Flat f) u) (\lambda (ee:
 C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow 
 False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C 
 c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 523
+END *)
 
 theorem wf3_gen_bind1:
  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (b: 
@@ -182,6 +185,9 @@ T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda
 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
 O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g 
 c1 v w) \to False))))) H4))))))))) y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2507
+END *)
 
 theorem wf3_gen_flat1:
  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (f: 
@@ -230,6 +236,9 @@ C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
 (\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) H2 c1 H8) 
 in (let H10 \def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H8) in 
 H10))))) H5)) H4))))))))) y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 737
+END *)
 
 theorem wf3_gen_head2:
  \forall (g: G).(\forall (x: C).(\forall (c: C).(\forall (v: T).(\forall (k: 
@@ -296,4 +305,7 @@ C c2 (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (ex B (\lambda (b: B).(eq
 K k (Bind b)))))) H2 (CHead c k v) H4) in (let H6 \def (eq_ind C c2 (\lambda 
 (c0: C).(wf3 g c1 c0)) H1 (CHead c k v) H4) in (H5 (refl_equal C (CHead c k 
 v))))))))))))) x y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1225
+END *)