X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpc3%2Ffsubst0.ma;h=c563ca397d1d2a3791f92cc065f1f8d178562f91;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=6a2cda2f6001338e2994c0071dc9f04e48599452;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/fsubst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/fsubst0.ma
index 6a2cda2f6..c563ca397 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/fsubst0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/fsubst0.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pc3/left.ma".
+include "Basic-1/pc3/left.ma".
 
-include "LambdaDelta-1/fsubst0/defs.ma".
+include "Basic-1/fsubst0/defs.ma".
 
-include "LambdaDelta-1/csubst0/getl.ma".
+include "Basic-1/csubst0/getl.ma".
 
 theorem pc3_pr2_fsubst0:
  \forall (c1: C).(\forall (t1: T).(\forall (t: T).((pr2 c1 t1 t) \to (\forall 
@@ -341,6 +341,9 @@ H6) t0 t0 (pr0_refl t0) x H24)))))))) (subst0_subst0_back t3 t0 u i H2 x4 u0
 t0 (pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i (csubst0_getl_ge i0 i H7 c c0 u0 
 H5 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0 H2))))))))))) c2 t4 
 H3)))))))))))))))) c1 t1 t H)))).
+(* COMMENTS
+Initial nodes: 6455
+END *)
 
 theorem pc3_pr2_fsubst0_back:
  \forall (c1: C).(\forall (t: T).(\forall (t1: T).((pr2 c1 t t1) \to (\forall 
@@ -652,6 +655,9 @@ t0 u i H2 x4 u0 (minus i0 (S i)) H19)))))))) H15)) H14))))))))))) H9)) H8)))
 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n 
 i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5 
 H4))))))))))) c2 t4 H3)))))))))))))))) c1 t t1 H)))).
+(* COMMENTS
+Initial nodes: 6191
+END *)
 
 theorem pc3_fsubst0:
  \forall (c1: C).(\forall (t1: T).(\forall (t: T).((pc3 c1 t1 t) \to (\forall 
@@ -714,4 +720,7 @@ c0)).(\lambda (e: C).(\lambda (H6: (getl i c1 (CHead e (Bind Abbr)
 u))).(pc3_t t0 c0 t5 (pc3_s c0 t5 t0 (pc3_pr2_fsubst0_back c1 t0 t2 H0 i u c0 
 t5 (fsubst0_both i u c1 t2 t5 H4 c0 H5) e H6)) t3 (H2 i u c0 t0 (fsubst0_fst 
 i u c1 t0 c0 H5) e H6)))))))) c2 t4 H3)))))))))))) t1 t H)))).
+(* COMMENTS
+Initial nodes: 1249
+END *)