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