uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/fwd.ma
index 7a8e147abaf971f310c935356d06e16bd2190416..ed48846a8a56b55fd4a170dcb286c132ccc7447c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/aprem/defs.ma".
+include "Basic-1/aprem/defs.ma".
 
 theorem aprem_gen_sort:
  \forall (x: A).(\forall (i: nat).(\forall (h: nat).(\forall (n: nat).((aprem 
@@ -35,6 +35,9 @@ A).(\lambda (i0: nat).(\lambda (_: (aprem i0 a2 a)).(\lambda (_: (((eq A a2
 in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | 
 (AHead _ _) \Rightarrow True])) I (ASort h n) H3) in (False_ind False 
 H4))))))))) i y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 227
+END *)
 
 theorem aprem_gen_head_O:
  \forall (a1: A).(\forall (a2: A).(\forall (x: A).((aprem O (AHead a1 a2) x) 
@@ -68,6 +71,9 @@ a4 (AHead a1 a2)) \to (eq A a a1)))) H3 a2 H7) in (let H10 \def (eq_ind A a0
 (\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 A a 
 a1) H11)))))) H6)))))))))) y0 y x H1))) H0))) H)))).
+(* COMMENTS
+Initial nodes: 500
+END *)
 
 theorem aprem_gen_head_S:
  \forall (a1: A).(\forall (a2: A).(\forall (x: A).(\forall (i: nat).((aprem 
@@ -108,4 +114,7 @@ return (\lambda (_: nat).nat) with [O \Rightarrow i0 | (S n) \Rightarrow n]))
 (S i)) \to ((eq A a2 (AHead a1 a2)) \to (aprem i a2 a)))) H9 i H11) in (let 
 H13 \def (eq_ind nat i0 (\lambda (n: nat).(aprem n a2 a)) H10 i H11) in 
 H13))))))) H6)))))))))) y0 y x H1))) H0))) H))))).
+(* COMMENTS
+Initial nodes: 631
+END *)