(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/drop1/fwd.ma".
+include "Basic-1/drop1/fwd.ma".
-include "LambdaDelta-1/drop/props.ma".
+include "Basic-1/drop/props.ma".
-include "LambdaDelta-1/getl/defs.ma".
+include "Basic-1/getl/defs.ma".
theorem drop1_skip_bind:
\forall (b: B).(\forall (e: C).(\forall (hds: PList).(\forall (c:
e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead x (Bind b)
(lift1 p u)) n (S n0) (drop_skip_bind n n0 c x H2 b (lift1 p u)) (CHead e
(Bind b) u) (Ss p) (H x u H3))))) H1)))))))))) hds))).
+(* COMMENTS
+Initial nodes: 379
+END *)
theorem drop1_cons_tail:
\forall (c2: C).(\forall (c3: C).(\forall (h: nat).(\forall (d: nat).((drop
(PCons n n0 (PConsTail p h d)) c1 c3) (\lambda (x: C).(\lambda (H3: (drop n
n0 c1 x)).(\lambda (H4: (drop1 p x c2)).(drop1_cons c1 x n n0 H3 c3
(PConsTail p h d) (H0 x H4))))) H2))))))))) hds)))))).
+(* COMMENTS
+Initial nodes: 271
+END *)
theorem drop1_trans:
\forall (is1: PList).(\forall (c1: C).(\forall (c0: C).((drop1 is1 c1 c0)
c2) (\lambda (x: C).(\lambda (H3: (drop n n0 c1 x)).(\lambda (H4: (drop1 p x
c0)).(drop1_cons c1 x n n0 H3 c2 (papp p is2) (H x c0 H4 is2 c2 H1)))))
H2))))))))))))) is1).
+(* COMMENTS
+Initial nodes: 287
+END *)