nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds:
PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons h d hds) c1
c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P p c c0 \def
nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds:
PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons h d hds) c1
c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P p c c0 \def