(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/clear/fwd.ma".
+include "Basic-1/clear/fwd.ma".
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
theorem drop_clear:
\forall (c1: C).(\forall (c2: C).(\forall (i: nat).((drop (S i) O c1 c2) \to
(Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e
c2)))) x0 x1 x2 (clear_flat c (CHead x1 (Bind x0) x2) H3 f t) H4)))))) H2))))
k (drop_gen_drop k c c2 t i H0))))))))) c1).
+(* COMMENTS
+Initial nodes: 770
+END *)
theorem drop_clear_O:
\forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (u: T).((clear c
F).(\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b)
u))).(drop_drop (Flat f) i c0 e2 (H e1 u (clear_gen_flat f c0 (CHead e1 (Bind
b) u) t H2) e2 i H1) t))) k H0))))))))))) c)).
+(* COMMENTS
+Initial nodes: 619
+END *)
theorem drop_clear_S:
\forall (x2: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop
u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b)
(lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))) k H1 H3) x1
H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).
+(* COMMENTS
+Initial nodes: 1449
+END *)