uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
index f8fae3129d2586d2ed9a268aebe0153a6c658d74..61fcb57992815c93b7b01af02664f084be2524ce 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/asucc/defs.ma".
+include "Basic-1/asucc/defs.ma".
 
 theorem asucc_gen_sort:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(\forall (a: A).((eq A 
@@ -39,6 +39,9 @@ n0)))))))).(\lambda (H1: (eq A (ASort h n) (asucc g (AHead a0 a1)))).(let H2
 False])) I (asucc g (AHead a0 a1)) H1) in (False_ind (ex_2 nat nat (\lambda 
 (h0: nat).(\lambda (n0: nat).(eq A (AHead a0 a1) (ASort h0 n0))))) H2))))))) 
 a)))).
+(* COMMENTS
+Initial nodes: 317
+END *)
 
 theorem asucc_gen_head:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((eq A 
@@ -90,4 +93,7 @@ a1 a4) (asucc g a3)) \to (ex2 A (\lambda (a5: A).(eq A a3 (AHead a1 a5)))
 a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3 
 (refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4)))) 
 H2))))))) a)))).
+(* COMMENTS
+Initial nodes: 957
+END *)