I thought it was clear. I would start with 1, not 0 for the first example of the derivation of Natural numbers via succession or the related Peano axiom. I know some texts start with 1 and others 0, but given counting most likely started with objects, it is more fundamental to begin with 1. The concept of nothing or zero just seems an abstract step away. Nice treatment of the lambda calculus.