X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fwcpr0%2Ffwd.ma;h=2b0531a8a15d71ff0306f92c893e030cea62257f;hb=c6ec0dc44c2e592c7b1323304052bc1a523e7c22;hp=7005751af3c113d0c4675252aa1aec10bd0d232e;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

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 7005751af..2b0531a8a 100644
--- 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 *)