uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/fwd.ma
index e32fb9340a7ec15920c8729f5b78f1f35881d916..48495c148a67a2cf625c31e68c338d4544ec1059 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/drop/defs.ma".
+include "Basic-1/drop/defs.ma".
 
 theorem drop_gen_sort:
  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(\forall (x: C).((drop 
@@ -46,6 +46,9 @@ u)) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort
 _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in 
 (False_ind (and3 (eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))) (eq 
 nat h0 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 595
+END *)
 
 theorem drop_gen_refl:
  \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
@@ -76,6 +79,9 @@ H9 \def (eq_ind nat (S d) (\lambda (ee: nat).(match ee in nat return (\lambda
 (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) 
 in (False_ind (eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)) H9)) h 
 H6)))))))))))))) y y0 x e H1))) H0))) H))).
+(* COMMENTS
+Initial nodes: 561
+END *)
 
 theorem drop_gen_drop:
  \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: 
@@ -163,6 +169,9 @@ c e))))) H19 (lift (S h) (r k d) u0) H18) in (let H22 \def (eq_ind nat (S d)
 \Rightarrow False | (S _) \Rightarrow True])) I O H6) in (False_ind (drop (r 
 k h) (S d) c (CHead e k u0)) H22))) k0 H14))))))))) H12)) H11)))))))))))))))) 
 y1 y0 y x H2))) H1))) H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1856
+END *)
 
 theorem drop_gen_skip_r:
  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall 
@@ -242,6 +251,9 @@ c)))) (ex_intro2 C (\lambda (e0: C).(eq C (CHead c0 k (lift h0 (r k d) u))
 (CHead e0 k (lift h0 (r k d) u)))) (\lambda (e0: C).(drop h0 (r k d) e0 c)) 
 c0 (refl_equal C (CHead c0 k (lift h0 (r k d) u))) H17) d0 H15)))) k0 H9))))) 
 u0 H8)))) H7)) H6)))))))))))) h y0 x y H1))) H0))) H))))))).
+(* COMMENTS
+Initial nodes: 1758
+END *)
 
 theorem drop_gen_skip_l:
  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall 
@@ -366,4 +378,7 @@ T (lift h0 (r k d) u0) (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_:
 T).(drop h0 (r k d) c e0))) e u0 (refl_equal C (CHead e k u0)) (refl_equal T 
 (lift h0 (r k d) u0)) H19) d0 H17)))) u H13)) k0 H9))))))))) H7)) 
 H6)))))))))))) h y0 y x H1))) H0))) H))))))).
+(* COMMENTS
+Initial nodes: 2574
+END *)