uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/props.ma
index 895bc51769029100b2a8e254d52ae35eb06e14eb..fb83210624ef7643d1de9c49b699518e030a509b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/aprem/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/aprem/fwd.ma".
+include "Basic-1/aprem/fwd.ma".
 
-include "LambdaDelta-1/leq/defs.ma".
+include "Basic-1/leq/defs.ma".
 
 theorem aprem_repl:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall 
@@ -55,6 +55,9 @@ A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1))) (\lambda
 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 
 a4) b1)) x H7 (aprem_succ a4 x i0 H8 a0))))) H6))))))) i H4)))))))))))) a1 a2 
 H)))).
+(* COMMENTS
+Initial nodes: 621
+END *)
 
 theorem aprem_asucc:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i 
@@ -67,4 +70,7 @@ A).(aprem_zero a0 (asucc g a3)))) (\lambda (a0: A).(\lambda (a: A).(\lambda
 (i0: nat).(\lambda (_: (aprem i0 a0 a)).(\lambda (H1: (aprem i0 (asucc g a0) 
 a)).(\lambda (a3: A).(aprem_succ (asucc g a0) a i0 H1 a3))))))) i a1 a2 
 H))))).
+(* COMMENTS
+Initial nodes: 101
+END *)