Пример умножения m * n

m⌉ * ⌈n⌉ ≡ λf x.⌈m⌉ (⌈n⌉ f) x ; def *
≡ λf x.(λg x.gm x) (⌈n⌉ f) x ; def ⌈m⌉
= λf x.(λx.(⌈n⌉ f)m x) x ; →β
= λf x.(λy.(⌈n⌉ f)m y) x ; →α
= λf x.((⌈n⌉ f)m x) ; →β
= λf x.(((λh x.hn x) f)m x) ; def ⌈n⌉
= λf x.(λx.fn x)m x ; →β
= λf x.(fn)m x ; →β
= λf x.fnm x ; def композиции