DEFINITION drop1_cons_tail()
TYPE =
       ∀c2:C
         .∀c3:C
           .∀h:nat
             .∀d:nat
               .(drop h d c2 c3)→∀hds:PList.∀c1:C.(drop1 hds c1 c2)→(drop1 (PConsTail hds h d) c1 c3)
BODY =
Show proof