DEFINITION drop1_trans()
TYPE =
       ∀is1:PList.∀c1:C.∀c0:C.(drop1 is1 c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp is1 is2) c1 c2)
BODY =
Show proof