update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / csubst1 / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubst1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/csubst1/props.ma
index 518a865649646e32fba70256adf337d37457fcf8..349485a88c5d45a45d25e98e126852c4a89ebccd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/csubst1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubst1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/csubst1/defs.ma".
+include "basic_1/csubst1/fwd.ma".
 
-include "Basic-1/subst1/defs.ma".
+include "basic_1/subst1/fwd.ma".
 
 theorem csubst1_head:
  \forall (k: K).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
@@ -38,9 +38,6 @@ 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 
@@ -54,9 +51,6 @@ 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 
@@ -69,7 +63,4 @@ 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 *)