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