DEFINITION Ss()
TYPE =
       PList→PList
BODY =
Show proof