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