DEFINITION s()
TYPE =
       K→nat→nat
BODY =
Show proof