DEFINITION wadd()
TYPE =
       (nat→nat)→nat→nat→nat
BODY =
λf:nat→nat.λw:nat.λn:nat.<λn1:nat.nat> CASE n OF O⇒w | S m⇒f m