uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fsubst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fsubst0.ma
index c85e929eb0c8a45d985785f75bfdf07679732f5e..f92366a26373a5f25736f4976b80e0fc8bc432db 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fsubst0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fsubst0.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/fsubst0.ma".
+include "Basic-1/pc3/fsubst0.ma".
 
-include "LambdaDelta-1/getl/getl.ma".
+include "Basic-1/getl/getl.ma".
 
 theorem ty3_fsubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1 
@@ -959,6 +959,9 @@ Cast) t0 t3)) i u c3 (THead (Flat Cast) t0 x0) (fsubst0_both i u c (THead
 i H10 t0) c3 H6) e H7)))) (ty3_correct g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst 
 i u c t3 c3 H6) e H7))) t5 H9)))))) H8)) (subst0_gen_head (Flat Cast) u t3 t2 
 t5 i H5)))))))) c2 t4 H4)))))))))))))) c1 t1 t H))))).
+(* COMMENTS
+Initial nodes: 23439
+END *)
 
 theorem ty3_csubst0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
@@ -971,6 +974,9 @@ c2 t1 t2)))))))))))
 nat).(\lambda (H0: (getl i c1 (CHead e (Bind Abbr) u))).(\lambda (c2: 
 C).(\lambda (H1: (csubst0 i u c1 c2)).(ty3_fsubst0 g c1 t1 t2 H i u c2 t1 
 (fsubst0_fst i u c1 t1 c2 H1) e H0))))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem ty3_subst0:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((ty3 g c t1 
@@ -983,4 +989,7 @@ t)))))))))))
 (H0: (getl i c (CHead e (Bind Abbr) u))).(\lambda (t2: T).(\lambda (H1: 
 (subst0 i u t1 t2)).(ty3_fsubst0 g c t1 t H i u c t2 (fsubst0_snd i u c t1 t2 
 H1) e H0))))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)