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