(* 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
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
(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
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
(\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 *)