Операции над нумералами - последователь

Suc ≡ λx y z.y (x y z): Операция прибавления единицы к нумералу Чёрча.

В самом деле:

Suc ⌈`n`⌉ ≡ (λx y z.y (x y z)) (λf x.fⁿ x)	; def Suc и нумерала
= λy z.y (((λf x.fⁿ x) y) z)	; →_β, редекс - всё
= λy z.y ((λx.yⁿ x) z)	; →_β
= λy z.y (yⁿ z)	; →_β
≡ λy z.y^{n + 1} z	; def композиции
≡ ⌈`n` + 1⌉	; def нумерала