succ=\n.\f.\x.f((nf)x)