X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubst0%2Fclear.ma;h=0700d7d482c79992303197ff2676df8cee85e1e9;hb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;hp=cf1e0e68e058f0814e3efe1e295281cd6fdee0b2;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/clear.ma
index cf1e0e68e..0700d7d48 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/clear.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubst0/props.ma".
+include "Basic-1/csubst0/props.ma".
 
-include "LambdaDelta-1/csubst0/fwd.ma".
+include "Basic-1/csubst0/fwd.ma".
 
-include "LambdaDelta-1/clear/fwd.ma".
+include "Basic-1/clear/fwd.ma".
 
 theorem csubst0_clear_O:
  \forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 O v c1 c2) \to 
@@ -102,6 +102,9 @@ x1)) H6 O H8) in (let H10 \def (eq_ind_r nat x2 (\lambda (n: nat).(subst0 n v
 t x0)) H5 O H8) in (clear_flat x1 c0 (H x1 v H9 c0 (clear_gen_flat f c c0 t 
 H7)) f x0)))))) k H1 H3) c2 H4)))))))) H2)) (csubst0_gen_head k c c2 t v O 
 H0))))))))))) c1).
+(* COMMENTS
+Initial nodes: 1582
+END *)
 
 theorem csubst0_clear_O_back:
  \forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 O v c1 c2) \to 
@@ -186,6 +189,9 @@ nat).(csubst0 n v c x1)) H6 O H8) in (let H11 \def (eq_ind_r nat x2 (\lambda
 (n: nat).(subst0 n v t x0)) H5 O H8) in (clear_flat c c0 (H x1 v H10 c0 
 (clear_gen_flat f x1 c0 x0 H9)) f t)))))) k H3 H7))))))))) H2)) 
 (csubst0_gen_head k c c2 t v O H0))))))))))) c1).
+(* COMMENTS
+Initial nodes: 1606
+END *)
 
 theorem csubst0_clear_S:
  \forall (c1: C).(\forall (c2: C).(\forall (v: T).(\forall (i: nat).((csubst0 
@@ -1026,6 +1032,9 @@ u2)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
 T).(\lambda (_: T).(csubst0 i v e1 e2)))))) x3 x4 x5 x6 x7 H14 (clear_flat x1 
 (CHead x5 (Bind x3) x7) H15 f x0) H16 H17))))))))))) H13)) H12)))))))) k H1 
 H3) c2 H4)))))))) H2)) (csubst0_gen_head k c c2 t v (S i) H0)))))))))))) c1).
+(* COMMENTS
+Initial nodes: 14968
+END *)
 
 theorem csubst0_clear_trans:
  \forall (c1: C).(\forall (c2: C).(\forall (v: T).(\forall (i: nat).((csubst0 
@@ -1124,4 +1133,7 @@ e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1))) (ex_intro2 C
 (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 
 (Flat f) u1) e1)) x H7 (clear_flat c3 x H8 f u1)))))) H6)) H5))))) k 
 H3))))))))))))) i v c1 c2 H))))).
+(* COMMENTS
+Initial nodes: 2085
+END *)