DEFINITION papp_ss()
TYPE =
       ∀is1:PList.∀is2:PList.(eq PList (papp (Ss is1) (Ss is2)) (Ss (papp is1 is2)))
BODY =
Show proof