We use the substitution model to find what are
two in the Church numerals representation.
So we can now define
We do the same thing to find what is
So the definition of
We can now have an idea of how Church numerals are working. We can define the addition as bellow.