uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop1/fwd.ma
index 665cf9da42e2b00a84a7ef60810661f040ce5935..6e4d1789e832997e10cb8be5ae44488a6fdd0b68 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop1/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop1/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/drop1/defs.ma".
+include "Basic-1/drop1/defs.ma".
 
 theorem drop1_gen_pnil:
  \forall (c1: C).(\forall (c2: C).((drop1 PNil c1 c2) \to (eq C c1 c2)))
@@ -32,6 +32,9 @@ PList).(\lambda (_: (drop1 hds c4 c5)).(\lambda (_: (((eq PList hds PNil) \to
 (\lambda (_: PList).Prop) with [PNil \Rightarrow False | (PCons _ _ _) 
 \Rightarrow True])) I PNil H4) in (False_ind (eq C c3 c5) H5)))))))))))) y c1 
 c2 H0))) H))).
+(* COMMENTS
+Initial nodes: 198
+END *)
 
 theorem drop1_gen_pcons:
  \forall (c1: C).(\forall (c3: C).(\forall (hds: PList).(\forall (h: 
@@ -72,4 +75,7 @@ PList).(drop1 p c4 c5)) H2 hds H7) in (let H12 \def (eq_ind nat d0 (\lambda
 (n: nat).(drop n d c2 c4)) H12 h H9) in (ex_intro2 C (\lambda (c6: C).(drop h 
 d c2 c6)) (\lambda (c6: C).(drop1 hds c6 c5)) c4 H13 H11)))))))) H6)) 
 H5)))))))))))) y c1 c3 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 587
+END *)