uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/props.ma
index 569bde181d05ac4a5554a4feb00e2052519ba7cd..0834a7afeb5e57b68fc03d8f2ce80e136e10a6fc 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/cimp/defs.ma".
+include "Basic-1/cimp/defs.ma".
 
-include "LambdaDelta-1/getl/getl.ma".
+include "Basic-1/getl/getl.ma".
 
 theorem cimp_flat_sx:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp (CHead c (Flat f) v) 
@@ -35,6 +35,9 @@ w) H0))))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c (Flat f) v)
 b) w))))))).(\lambda (H0: (getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind 
 b) w))).(ex_intro C (\lambda (d2: C).(getl (S h0) c (CHead d2 (Bind b) w))) 
 d1 (getl_gen_S (Flat f) c (CHead d1 (Bind b) w) v h0 H0))))) h H)))))))).
+(* COMMENTS
+Initial nodes: 327
+END *)
 
 theorem cimp_flat_dx:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp c (CHead c (Flat f) 
@@ -44,6 +47,9 @@ v))))
 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h c (CHead d1 (Bind 
 b) w))).(ex_intro C (\lambda (d2: C).(getl h (CHead c (Flat f) v) (CHead d2 
 (Bind b) w))) d1 (getl_flat c (CHead d1 (Bind b) w) h H f v))))))))).
+(* COMMENTS
+Initial nodes: 83
+END *)
 
 theorem cimp_bind:
  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall 
@@ -87,6 +93,9 @@ in (ex_ind C (\lambda (d2: C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C
 (\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))) 
 x (getl_head (Bind b) h0 c2 (CHead x (Bind b0) w) H3 v)))) H2)))))) h 
 H0)))))))))).
+(* COMMENTS
+Initial nodes: 817
+END *)
 
 theorem cimp_getl_conf:
  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall 
@@ -124,4 +133,7 @@ nat).(getl (minus n i) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0))) (H_y0
 b) w) (CHead x0 (Bind b0) w0))) H7 (S h) (minus_plus_r (S h) i)) in (ex_intro 
 C (\lambda (d2: C).(getl h x (CHead d2 (Bind b0) w0))) x0 (getl_gen_S (Bind 
 b) x (CHead x0 (Bind b0) w0) w h H8)))))))) H4))))))))) H2))) H1)))))))))).
+(* COMMENTS
+Initial nodes: 673
+END *)