Lambda definition of the successor function
= Lambda definition of the successor function
The <successor function> is lambda-defined on <Church numeral>[Church numerals] by
$$
\operatorname{Succ}=\lambda n.\lambda f.\lambda x.f(nfx),
$$
because $\operatorname{Succ}\,c_n\equiv_\beta c_{n+1}$.