(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubc/fwd.ma".
+include "Basic-1/csubc/fwd.ma".
-include "LambdaDelta-1/sc3/props.ma".
+include "Basic-1/sc3/props.ma".
theorem csubc_drop_conf_O:
\forall (g: G).(\forall (c1: C).(\forall (e1: C).(\forall (h: nat).((drop h
e1 x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x1 (Bind x0) x2)
e2)) (\lambda (e2: C).(csubc g e1 e2)) x (drop_drop (Bind x0) n x1 x H12 x2)
H13)))) H11))))) c2 H5)))))))) H4)) H3)))))))) h))))))) c1)).
+(* COMMENTS
+Initial nodes: 2389
+END *)
theorem drop_csubc_trans:
\forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
x2 x4) (csubc_void g c x H19 x2 H13 (lift h (r (Bind Void) n) x1) (lift h n
x4)))))) H17))) k H12))) e1 H11)))))))) H10)) H9))) t H4)))))))))
(drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).
+(* COMMENTS
+Initial nodes: 3747
+END *)
theorem csubc_drop_conf_rev:
\forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
(drop_skip_bind h n x x3 H18 Void x4) (csubc_void g x c H19 x2 H13 (lift h n
x4) (lift h (r (Bind x2) n) x1)))))) H17))) k H12))) e1 H11)))))))) H10))
H9))) t H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).
+(* COMMENTS
+Initial nodes: 3747
+END *)