(λ p q . p)(λ x y . y)(λ x y . x) ⇒ (λ q x y. y)(λ x y . x) ⇒ λ x y. y
(λ p q. p p q) (λ x y . x) (λ x y . y) ⇒ (λ q. (λ x y . x) (λ x y . x) q) (λ x y . y) ⇒ (λ x y . x) (λ x y . x) (λ x y . y) ⇒ (λ z x y . x) (λ x y . y) ⇒ λ x y . x
(λ m n f . m (n f)) (λ s z . s z) (λ s z . z) ⇒ (λ n f . (λ s z . s z) (n f)) (λ s z . z) ⇒ λ f . (λ s z . s z) ((λ s z . z) f) ⇒ λ f z. (λ s z . z) f z ⇒ λ f z. (λ z . z) z ⇒ λ f z. z