Proposition 1.8.1.6.  Let n ∈ . Then:
Proof.  Trivial.
Remarks.

This proposition justifies the notation for the successor constructor.

References.