DEFINITION ptrans()
TYPE =
       PList→nat→PList
BODY =
FIXptrans{
         ptrans:PList→nat→PList
         :=λhds:PList
           .λi:nat
             .<λp:PList.PList>
               CASE hds OF
                 PNil⇒PNil
               | PCons h d hds0⇒
                     let j := trans hds0 i
                     in let q := ptrans hds0 i
                          in <λb:bool.PList>
                                 CASE blt j d OF
                                   true⇒PCons h (minus d (S j)) q
                                 | false⇒q
         }