Proposition 1.8.1.39 (Induction principle (property-based)).  Let p be a property on  such that p(0) and [∀ m ∈  s.t. p(m) : p(m + 1)], n ∈ . Then:
Proof.  By induction on n.
Remarks.

This is a formulation of the induction principle based on the definition of a property (see $../../Properties/Properties). In HLM, it is provable from structural induction.

References.