(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
-include "LambdaDelta-1/r/props.ma".
+include "Basic-1/r/props.ma".
theorem drop_skip_bind:
\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
(H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
(Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
+(* COMMENTS
+Initial nodes: 95
+END *)
theorem drop_skip_flat:
\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead
e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S
d))))))))).
+(* COMMENTS
+Initial nodes: 101
+END *)
theorem drop_S:
\forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h:
u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0:
nat).(drop n0 O c0 e)) (H e u (r k n) (drop_gen_drop k c0 (CHead e (Bind b)
u) t n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
+(* COMMENTS
+Initial nodes: 807
+END *)
theorem drop_ctail:
\forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop
(drop_skip k h n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u)
x1) t H2)) c3 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d)))))))
c1).
+(* COMMENTS
+Initial nodes: 1211
+END *)
theorem drop_mono:
\forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h
H5 x4 H8)) (refl_equal K k) (refl_equal T x3)) x5 (lift_inj x5 x3 h (r k n)
H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k H1)))))))
(drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).
+(* COMMENTS
+Initial nodes: 1539
+END *)
theorem drop_conf_lt:
\forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall
H8)))))) (H0 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e
H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2)))))))))
k0)))) c)))))) i)).
+(* COMMENTS
+Initial nodes: 2972
+END *)
theorem drop_conf_ge:
\forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to
(minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5))))) e
H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2 H3)))))))))
k)))) c))))) i).
+(* COMMENTS
+Initial nodes: 2726
+END *)
theorem drop_conf_rev:
\forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
f) t))) (CHead x (Flat f) (lift i (r (Flat f) j0) t)) (drop_drop (Flat f) j0
x c2 H3 (lift i (r (Flat f) j0) t)) (drop_skip (Flat f) i j0 x e2 H4 t)))))
H2))))) k (drop_gen_drop k e2 e3 t j0 H))))))))))) e1)))) j).
+(* COMMENTS
+Initial nodes: 1154
+END *)
theorem drop_trans_le:
\forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1))
H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3)))))))
(drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).
+(* COMMENTS
+Initial nodes: 2453
+END *)
theorem drop_trans_ge:
\forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
f) i0) O x0 e2)).(IHc x0 (r (Flat f) d0) h H8 e2 H9 H1)))) k H4
(drop_gen_drop k x0 e2 x1 i0 H6)) (lift h (r k d0) x1)) t H3)))))))))
(drop_gen_skip_l c2 c3 t h d0 k H))))))))) d))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 2020
+END *)