main(x,y) = add(x,y)

add(S(x),y) = S(add(x,y))
add(Z,y)    = idNat(y)
idNat(S(x)) = S(s) where s = idNat(x)
idNat(Z)    = Z
