INDUCTIVE DEFINITION drop1 () [ ]
OF ARITY PList→C→C→Prop
BUILT FROM:
     drop1_nil: ∀c:C.(drop1 PNil c c)
   | drop1_cons: ∀c1:C
                           .∀c2:C
                             .∀h:nat
                               .∀d:nat.(drop h d c1 c2)→∀c3:C.∀hds:PList.(drop1 hds c2 c3)→(drop1 (PCons h d hds) c1 c3)