DEFINITION wadd()
TYPE =
       (nat→nat)→nat→nat→nat
BODY =
Show proof