uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / ty3 / subst1.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/subst1.ma
index 9c1ecb7116c38296480c1e98a1fef431276fa326..ca9516e589b7b1080fb9416827fe5d052088f7e8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/subst1.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/props.ma".
+include "Basic-1/ty3/props.ma".
 
-include "LambdaDelta-1/pc3/subst1.ma".
+include "Basic-1/pc3/subst1.ma".
 
-include "LambdaDelta-1/getl/getl.ma".
+include "Basic-1/getl/getl.ma".
 
 theorem ty3_gen_cabbr:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
@@ -552,6 +552,9 @@ H12) (lift (S O) d (THead (Flat Cast) x0 x2)) (lift_flat Cast x0 x2 (S O) d))
 O) d x1) d H9 (Flat Cast) t4 (lift (S O) d x0) H8) (lift (S O) d (THead (Flat 
 Cast) x1 x0)) (lift_flat Cast x1 x0 (S O) d)) (ty3_cast g a x2 x0 H15 x1 
 H10)))))))) H11))))))) H7)))))))))))))))))) c t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 12848
+END *)
 
 theorem ty3_gen_cvoid:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
@@ -1093,4 +1096,7 @@ x2 x0 H19 x1 H9)) (THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0))
 (lift_flat Cast x1 x0 (S O) d)) (THead (Flat Cast) (lift (S O) d x0) (lift (S 
 O) d x2)) (lift_flat Cast x0 x2 (S O) d))) t3 H15))))))) H14)) t4 H7)))) t0 
 H8))))))) H6)))))))))))))))) c t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 13105
+END *)