uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/fwd.ma
index 7005751af3c113d0c4675252aa1aec10bd0d232e..2b0531a8a15d71ff0306f92c893e030cea62257f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wcpr0/defs.ma".
+include "Basic-1/wcpr0/defs.ma".
 
 theorem wcpr0_gen_sort:
  \forall (x: C).(\forall (n: nat).((wcpr0 (CSort n) x) \to (eq C x (CSort 
@@ -34,6 +34,9 @@ c1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I 
 (CSort n) H4) in (False_ind (eq C (CHead c2 k u2) (CHead c1 k u1)) 
 H5))))))))))) y x H0))) H))).
+(* COMMENTS
+Initial nodes: 249
+END *)
 
 theorem wcpr0_gen_head:
  \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).((wcpr0 
@@ -96,4 +99,7 @@ C (CHead c2 k u2) (CHead c3 k u3)))) (\lambda (c3: C).(\lambda (_: T).(wcpr0
 c1 c3))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) c2 u2 (refl_equal C 
 (CHead c2 k u2)) H12 H10)) c0 H9))) u0 H7)) k0 H8)))) H6)) H5))))))))))) y x 
 H0))) H))))).
+(* COMMENTS
+Initial nodes: 1133
+END *)