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