uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/arity.ma
index 9fe69d76692f9cbd23b064319cd6d8d835814ef3..98770d9e9d0e7f3f0318daeb1885d9acf1fe33e0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/arity.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/nf2/fwd.ma".
+include "Basic-1/nf2/fwd.ma".
 
-include "LambdaDelta-1/arity/subst0.ma".
+include "Basic-1/arity/subst0.ma".
 
 theorem arity_nf2_inv_all:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t 
@@ -490,4 +490,7 @@ x1)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
 nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef 
 i)))) x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H7 H8)) t0 
 H6)))))) H5)) H4))))))))))) c t a H))))).
+(* COMMENTS
+Initial nodes: 9193
+END *)