X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubst1%2Fprops.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubst1%2Fprops.ma;h=518a865649646e32fba70256adf337d37457fcf8;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=9a8b4a2bbee0546b60c6696b5b2eaf6daa486ae3;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst1/props.ma
index 9a8b4a2bb..518a86564 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubst1/defs.ma".
+include "Basic-1/csubst1/defs.ma".
 
-include "LambdaDelta-1/subst1/defs.ma".
+include "Basic-1/subst1/defs.ma".
 
 theorem csubst1_head:
  \forall (k: K).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
@@ -38,6 +38,9 @@ c2)).(csubst1_ind i v c1 (\lambda (c: C).(csubst1 (s k i) v (CHead c1 k u1)
 (csubst0_snd k i v u1 t2 H0 c1)) (\lambda (c3: C).(\lambda (H2: (csubst0 i v 
 c1 c3)).(csubst1_sing (s k i) v (CHead c1 k u1) (CHead c3 k t2) (csubst0_both 
 k i v u1 t2 H0 c1 c3 H2)))) c2 H1)))))) u2 H)))))).
+(* COMMENTS
+Initial nodes: 365
+END *)
 
 theorem csubst1_bind:
  \forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
@@ -51,6 +54,9 @@ C).(\lambda (H0: (csubst1 i v c1 c2)).(eq_ind nat (s (Bind b) i) (\lambda (n:
 nat).(csubst1 n v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2))) 
 (csubst1_head (Bind b) i v u1 u2 H c1 c2 H0) (S i) (refl_equal nat (S 
 i))))))))))).
+(* COMMENTS
+Initial nodes: 107
+END *)
 
 theorem csubst1_flat:
  \forall (f: F).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
@@ -63,4 +69,7 @@ u2))))))))))
 C).(\lambda (H0: (csubst1 i v c1 c2)).(eq_ind nat (s (Flat f) i) (\lambda (n: 
 nat).(csubst1 n v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2))) 
 (csubst1_head (Flat f) i v u1 u2 H c1 c2 H0) i (refl_equal nat i)))))))))).
+(* COMMENTS
+Initial nodes: 103
+END *)