DEFINITION Ss()
TYPE =
       PList→PList
BODY =
FIXSs{
         Ss:PList→PList
         :=λhds:PList
           .<λp:PList.PList>
             CASE hds OF
               PNil⇒PNil
             | PCons h d hds0⇒PCons h (S d) (Ss hds0)
         }