X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst%2Fprops.ma;h=3bad044e3198e9cb33d31e6bd5b1c4f489e7cbee;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=3797559a289283e58836fa70e3dbd2a00fe57e87;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst/props.ma
index 3797559a2..3bad044e3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst/fwd.ma".
+include "Basic-1/subst/fwd.ma".
 
-include "LambdaDelta-1/subst0/defs.ma".
+include "Basic-1/subst0/defs.ma".
 
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
 
 theorem subst_lift_SO:
  \forall (v: T).(\forall (t: T).(\forall (d: nat).(eq T (subst d v (lift (S 
@@ -55,6 +55,9 @@ t0 t1))) (eq_ind_r T (THead k (subst d v (lift (S O) d t0)) (subst (s k d) v
 (THead k (lift (S O) d t0) (lift (S O) (s k d) t1))) (subst_head k v (lift (S 
 O) d t0) (lift (S O) (s k d) t1) d)) (lift (S O) d (THead k t0 t1)) 
 (lift_head k t0 t1 (S O) d)))))))) t)).
+(* COMMENTS
+Initial nodes: 879
+END *)
 
 theorem subst_subst0:
  \forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall (d: nat).((subst0 
@@ -107,4 +110,7 @@ i) v0 t4)))) (refl_equal T (THead k (subst i v0 u2) (subst (s k i) v0 t4)))
 (subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4)) 
 (subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1 
 t3 i))))))))))))) d v t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1363
+END *)