uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Ground-1 / ext / tactics.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/tactics.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/tactics.ma
index 79551495d86e5e699ba5d1ef301cf0a87b74fbe1..766db9f1f48279c86aa1d2ae8435e84ebd8fd9a6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/tactics.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/tactics.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Base-1/preamble.ma".
+include "Ground-1/preamble.ma".
 
 theorem insert_eq:
  \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: 
@@ -24,6 +24,9 @@ theorem insert_eq:
  \lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G: 
 ((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to (G 
 y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
+(* COMMENTS
+Initial nodes: 45
+END *)
 
 theorem unintro:
  \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x: 
@@ -31,6 +34,9 @@ A).(P x))) \to (P a))))
 \def
  \lambda (A: Set).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda (H: 
 ((\forall (x: A).(P x)))).(H a)))).
+(* COMMENTS
+Initial nodes: 17
+END *)
 
 theorem xinduction:
  \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x: 
@@ -38,4 +44,7 @@ A).((eq A t x) \to (P x)))) \to (P t))))
 \def
  \lambda (A: Set).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda (H: 
 ((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))).
+(* COMMENTS
+Initial nodes: 31
+END *)