uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / csuba / arity.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/arity.ma
index 7b5623ac844183f572c6ecfaccc6c1d5c35bad19..fe021cd0f3d05df8f88e29a6a0056ce28164e531 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/arity.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csuba/getl.ma".
+include "Basic-1/csuba/getl.ma".
 
-include "LambdaDelta-1/csuba/props.ma".
+include "Basic-1/csuba/props.ma".
 
-include "LambdaDelta-1/arity/props.ma".
+include "Basic-1/arity/props.ma".
 
-include "LambdaDelta-1/csubv/getl.ma".
+include "Basic-1/csubv/getl.ma".
 
 theorem csuba_arity:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
@@ -100,6 +100,9 @@ H4)))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_:
 g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: 
 C).(\lambda (H3: (csuba g c c2)).(arity_repl g c2 t0 a1 (H1 c2 H3) a2 
 H2)))))))))) c1 t a H))))).
+(* COMMENTS
+Initial nodes: 1505
+END *)
 
 theorem csuba_arity_rev:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
@@ -287,6 +290,9 @@ C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0 a1)))))).(\lambda
 (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (csuba g 
 c2 c)).(\lambda (H4: (csubv c2 c)).(arity_repl g c2 t0 a1 (H1 c2 H3 H4) a2 
 H2))))))))))) c1 t a H))))).
+(* COMMENTS
+Initial nodes: 3597
+END *)
 
 theorem arity_appls_appl:
  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (a1: A).((arity g c 
@@ -324,4 +330,7 @@ x)).(\lambda (H5: (arity g c (THeads (Flat Appl) t1 (THead (Bind Abbr) v t))
 (AHead x a2))).(arity_appl g c t0 x H4 (THeads (Flat Appl) t1 (THead (Flat 
 Appl) v (THead (Bind Abst) u t))) a2 (H1 (AHead x a2) H5))))) H3))))))) 
 vs))))))))).
+(* COMMENTS
+Initial nodes: 687
+END *)