(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubst0/fwd.ma".
+include "Basic-1/csubst0/fwd.ma".
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
-include "LambdaDelta-1/s/props.ma".
+include "Basic-1/s/props.ma".
theorem csubst0_drop_gt:
\forall (n: nat).(\forall (i: nat).((lt i n) \to (\forall (c1: C).(\forall
f) n0 x1 e (H12 x1 v H8 e H11) x0)))) H14)) (lt_gen_xS x2 n0 H13)))))) k
(drop_gen_drop k c e t n0 H3) H9 H10))) c2 H6)))))))) H4)) (csubst0_gen_head
k c c2 t v i H2))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 3092
+END *)
theorem csubst0_drop_gt_back:
\forall (n: nat).(\forall (i: nat).((lt i n) \to (\forall (c1: C).(\forall
x))).(\lambda (_: (lt x n0)).(drop_drop (Flat f) n0 c e (H12 x1 v H8 e H14)
t)))) H15)) (lt_gen_xS x2 n0 H13)))))) k H10 H11 (drop_gen_drop k x1 e x0 n0
H9)))))))))))) H4)) (csubst0_gen_head k c c2 t v i H2))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 2989
+END *)
theorem csubst0_drop_lt:
\forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall
x7) H16 x0) H17 H18)) e H15)))))))))) H14)) H13)))))) k (drop_gen_drop k c e
t n0 H2) H8 H9) i H4))) c2 H5)))))))) H3)) (csubst0_gen_head k c c2 t v i
H1))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 39886
+END *)
theorem csubst0_drop_eq:
\forall (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0
(Flat x3) x7) H15 x0) H16 H17)) e H14)))))))))) H13)) H12)))))))) k
(drop_gen_drop k c e t n0 H1) H3) c2 H4)))))))) H2)) (csubst0_gen_head k c c2
t v (S n0) H0))))))))))) c1)))) n).
+(* COMMENTS
+Initial nodes: 36162
+END *)
theorem csubst0_drop_eq_back:
\forall (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0
x3) x7)) (drop_drop (Flat f) n0 c (CHead x4 (Flat x3) x6) H16 t) H17 H18)) e
H15)))))))))) H14)) H13)))))))) k H3 (drop_gen_drop k x1 e x0 n0 H7))))))))))
H2)) (csubst0_gen_head k c c2 t v (S n0) H0))))))))))) c1)))) n).
+(* COMMENTS
+Initial nodes: 34765
+END *)
theorem csubst0_drop_lt_back:
\forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall
H16 (drop_drop (Flat f) n0 c x H17 t)))))) H15)) H14))))))) k H9 H10
(drop_gen_drop k x1 e2 x0 n0 H8)) i H4))))))))))) H3)) (csubst0_gen_head k c
c2 t v i H1))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 5939
+END *)