Мимолётом о числах Чёрча

Классическое определение числа Чёрча - эта функция, которая принимает два значения: функцию и аргумент. И применяет функцию к аргументу какое-то число раз.

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
n ≡ λf.λx. fn x

для таких чисел легко определить добавление единицы:

succ ≡ λn.λf.λx. n f (f x)

сложение двух чисел:

plus ≡ λm.λn.λf.λx m succ (n f x)

но вот вычитание или хотя-бы убавление на единицу реализовать довольно сложно. Википедия радует выносящей мозг записью

pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

Может быть я глуп, но осознать это я не смог. Но можно попробовать написать немного проще:
Для начала рассмотрим такую конструкцию

pair ≡ λf.λs.λc. c f s
fst ≡ λp. (λf.λs. f)
snd ≡ λp. (λf.λs. s)

Благодаря её можно создавать кортежи и обращаться к ним:

fst (pair x y) → x
snd (pair x y) → y

Теперь всё просто:

init ≡ pair 0 0
next ≡ λp. pair (snd p) (succ (snd p))
pred ≡ λn. fst (n next init)

мы строим ряд:

0 → (0, 0)
1 → (0, 1)
2 → (1, 2)
n → (n-1, n)

и беря первый аргумент подобной пары получаем число на единицу меньшее, чем было передано.