Types and Programming Languages - proof for theorem about principles of induction of terms

Question

Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4):

Suppose P is a predicate on terms.

Induction on depth:

If, for each term s, given P (r) for all r such that depth(r) < depth(s) we can show P(s), then P(s) holds for all s.

Proof of this theorem is left as the exercise for the reader. The solution to the exercise given in the book hints at defining a new predicate Q(n) on natural numbers such as:

∀s with depth(s) = n. P(s)

and apply the principle of complete induction on natural number (p. 19, axiom 2.4.2):

If, for each natural number n, given P(i) for all i < n we can show P(n), then P(n) holds for all n.

Since I lack experience in writing mathematical proofs, I'm struggling with applying the hint from the book and proving that theorem.

Given that:

• n = i + 1
• for all natural numbers i less than i + 1, the predicate Q(i) holds (from the induction axiom)

How do I prove that Q(n) (or Q(i + 1)) is true? Should I use depth function definition introduced previously for the simple arithmetic language?