Li-Fan Chen
says to
YSITD
add 0 x = x add (S x) y = add x (S y)