s (n s z)) c1 c3 → (λn. λs. λz. c1 s (n s z)) c3 → λs. λz. c1 s (c3 s z) → λs. λz. (λs’. λz’. s’ z’) s (c3 s z) → λs. λz. (λz’. s z’) (c3 s z) → λs. λz. s (c3 s z) → λs. λz. s ((λs’’. λz’’. s’’ (s’’ (s’’ z’’)) s z) → λs. λz. s ((λz’’. s (s (s z’’)) z) → λs. λz. s (s (s (s z))) → c4 ධՁͷྲྀΕ