Church numerals in and of themselves aren't that mind-blowing compared to finding out that the "predecessor" function can be written in lambda-I lambda calculus. lambda-I calculus is the variant where every bound variable has to make an appearance in the body of the lambda expression: %x.%y.x doesn't count as a valid expression since the bound variable 'y' doesn't appear in the body of the expression. Now, how do you find the predecessof of Church Numeral 3 (%f.%n.f (f (f n)))?
