Hello, this question is somewhat similar to the one I've asked some hours ago: I would like to have a predecessor operator PRED for the untyped lambda calculus that has the property that PRED (SUCC n) --> n (I) for a suitable successor function SUCC. So far I've tried with SUCC := S := \nfx.f (n f x) and PRED := P := \nfx.n (\gh.h (g f)) (\u.x) (\u.u) for which I can prove beta equivalence P (S n) == n by induction on n, but not the property (I). Could anybody give me a pointer? Greetings, ben ps. Please keep me in CC, since I'm not currently subscribed to the list.