[Haskell-beginners] pred (succ n)

[ben]

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.