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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/getl.ma
index e66c1c7a6..d3a109e0d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wcpr0/getl.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wcpr0/defs.ma".
+include "Basic-1/wcpr0/defs.ma".
 
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
 
 theorem wcpr0_drop:
  \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h: 
@@ -116,6 +116,9 @@ u0 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1 
 (drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k) 
 h)))))))))) c1 c2 H))).
+(* COMMENTS
+Initial nodes: 1755
+END *)
 
 theorem wcpr0_drop_back:
  \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h: 
@@ -215,6 +218,9 @@ x1 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1 
 (drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k) 
 h)))))))))) c2 c1 H))).
+(* COMMENTS
+Initial nodes: 1755
+END *)
 
 theorem wcpr0_getl:
  \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h: 
@@ -332,6 +338,9 @@ C).(\lambda (u3: T).(getl (S n) (CHead c4 (Flat f) u2) (CHead e2 k0 u3))))
 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda 
 (u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2) 
 H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
+(* COMMENTS
+Initial nodes: 2103
+END *)
 
 theorem wcpr0_getl_back:
  \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h: 
@@ -449,4 +458,7 @@ C).(\lambda (u3: T).(getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3))))
 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda 
 (u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1) 
 H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).
+(* COMMENTS
+Initial nodes: 2103
+END *)