DEFINITION ptrans()
TYPE =
       PList→nat→PList
BODY =
Show proof