DEFINITION drop1_gen_pcons()
TYPE =
       ∀c1:C
         .∀c3:C
           .∀hds:PList
             .∀h:nat.∀d:nat.(drop1 (PCons h d hds) c1 c3)→(ex2 C λc2:C.drop h d c1 c2 λc2:C.drop1 hds c2 c3)
BODY =
Show proof