uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/fwd.ma
index 3052659c06ae523120cea0ceaf48e73bbbe72b3e..9b3de2983a93f8056bb192511a9ebbdbb46cf87b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubst0/defs.ma".
+include "Basic-1/csubst0/defs.ma".
 
 theorem csubst0_gen_sort:
  \forall (x: C).(\forall (v: T).(\forall (i: nat).(\forall (n: nat).((csubst0 
@@ -44,6 +44,9 @@ c1 k u1) (CSort n))).(let H5 \def (eq_ind C (CHead c1 k u1) (\lambda (ee:
 C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow 
 False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H4) in (False_ind P 
 H5))))))))))))) i v y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 355
+END *)
 
 theorem csubst0_gen_head:
  \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall 
@@ -260,6 +263,9 @@ u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v0 u1
 u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v0 c1 
 c3)))) u2 c2 i0 (refl_equal nat (s k i0)) (refl_equal C (CHead c2 k u2)) H12 
 H11)) k0 H8))))))) H6)) H5))))))))))))) i v y x H0))) H))))))).
+(* COMMENTS
+Initial nodes: 4039
+END *)
 
 theorem csubst0_gen_S_bind_2:
  \forall (b: B).(\forall (x: C).(\forall (c2: C).(\forall (v: T).(\forall 
@@ -450,4 +456,7 @@ C).(\lambda (_: T).(csubst0 i v0 c3 c2))) (\lambda (c3: C).(\lambda (v1:
 T).(eq C (CHead c1 (Bind b) u1) (CHead c3 (Bind b) v1)))) c1 u1 H19 H18 
 (refl_equal C (CHead c1 (Bind b) u1)))))))) k H10)))))))) H8)) 
 H7)))))))))))))) y0 v x y H1))) H0))) H))))))).
+(* COMMENTS
+Initial nodes: 3878
+END *)