(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
-include "LambdaDelta-1/clear/drop.ma".
+include "Basic-1/clear/drop.ma".
theorem getl_drop:
\forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h:
(Bind b) 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) (getl_gen_S k c0 (CHead e (Bind b) u) t
n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
+(* COMMENTS
+Initial nodes: 827
+END *)
theorem getl_drop_conf_lt:
\forall (b: B).(\forall (c: C).(\forall (c0: C).(\forall (u: T).(\forall (i:
h d x3)) (getl_head k i0 x1 (CHead x4 (Bind b) x3) H23 x2) H24) u H22))))))))
H21)))))) e H11))))))))) (drop_gen_skip_l c0 e t h (plus (S i0) d) k
H9))))))) i H1 H7 IHx)))) k0 H5 H6))))))) x H3 H4)))) H2)))))))))))))) c)).
+(* COMMENTS
+Initial nodes: 6137
+END *)
theorem getl_drop_conf_ge:
\forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
a)) (getl (minus i h) e a) (\lambda (x: C).(\lambda (H3: (drop i O c
x)).(\lambda (H4: (clear x a)).(getl_intro (minus i h) e a x (drop_conf_ge i
x c H3 e h d H0 H1) H4)))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
theorem getl_conf_ge_drop:
\forall (b: B).(\forall (c1: C).(\forall (e: C).(\forall (u: T).(\forall (i:
u i H) c2 (S O) i H0 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(le n (S
i))) (le_n (S i)) (plus i (S O)) (plus_sym i (S O)))) i (minus_Sx_SO i)) in
H3)))))))).
+(* COMMENTS
+Initial nodes: 151
+END *)
theorem getl_drop_conf_rev:
\forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
e2)).(\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(\lambda (i:
nat).(\lambda (H0: (getl i c2 (CHead e2 (Bind b) v2))).(drop_conf_rev j e1 e2
H c2 (S i) (getl_drop b c2 e2 v2 i H0)))))))))).
+(* COMMENTS
+Initial nodes: 69
+END *)
theorem drop_getl_trans_lt:
\forall (i: nat).(\forall (d: nat).((lt i d) \to (\forall (c1: C).(\forall
(minus d (S i)) e1 e2)) x1 (getl_intro i c1 (CHead x1 (Bind b) (lift h (minus
d (S i)) v)) x0 H5 H9) H10)))) H8)))))) (drop_trans_le i d (le_S_n i d (le_S
(S i) d H)) c1 c2 h H0 x H3))))) H2)))))))))))).
+(* COMMENTS
+Initial nodes: 627
+END *)
theorem drop_getl_trans_le:
\forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d i) e0 e1)))
(\lambda (_: C).(\lambda (e1: C).(clear e1 e2))) x0 x H6 H7 H4)))) H5)))))
H2)))))))))).
+(* COMMENTS
+Initial nodes: 323
+END *)
theorem drop_getl_trans_ge:
\forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
(\lambda (e: C).(clear e e2)) (getl (plus i h) c1 e2) (\lambda (x:
C).(\lambda (H3: (drop i O c2 x)).(\lambda (H4: (clear x e2)).(getl_intro
(plus i h) c1 e2 x (drop_trans_ge i c1 c2 d h H x H3 H1) H4)))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
theorem getl_drop_trans:
\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl h c1 c2) \to
(Flat f) t) c3)).(\lambda (e2: C).(\lambda (i: nat).(\lambda (H1: (drop (S i)
O c3 e2)).(drop_drop (Flat f) (plus i (S n)) c2 e2 (IHc c3 (S n) (getl_gen_S
(Flat f) c2 c3 t n H0) e2 i H1) t))))))) h))))) k)))) c1).
+(* COMMENTS
+Initial nodes: 953
+END *)