Types and Programming Languages - proof for theorem about principles of induction of terms
While you should get in the habit of providing definitions so your question is self-contained, especially when the original text is not easily accessible, the first thing to note is that the theorem doesn't actually depend at all on what "terms" are or how "depth" is defined.

Given any set $S$ and any function $f:S\to\mathbb N$, the theorem will hold. That is, $$(\forall s\in S.(\forall r\in S.f(r) &lt; f(s) \to P(r))\to P(s))\to \forall s\in S.P(S)$$

How useful this theorem is depends on $f$. For example, if $f$ is a constant function then this theorem simplifies to $(\forall s\in S.P(s))\to(\forall s\in S.P(s))$ which isn't very useful.

To prove this via complete induction, you should, as is always a helpful strategy, write out the definitions, in this case, of complete induction. Complete induction states: $$(\forall n\in\mathbb N.(\forall m\in\mathbb N.m &lt; n\to Q(m))\to Q(n))\to\forall n\in\mathbb N.Q(n)$$

So the bulk of the task is choosing an appropriate $Q$ to get the result that you want. As the hint states, the fairly obvious choice is $Q(n)\equiv\forall s\in S.f(s)=n\to P(s)$. If you stick this $Q$ into the formula for complete induction, you can simplify it into the first formula. All the work comes down basically to showing that $\forall n\in\mathbb N.\forall s\in S.f(s)=n\to P(s)\iff\forall s\in S.P(s)$ which is a simple and  purely logical exercise. Indeed, we don't even need the fact that $\mathbb N$ is the naturals to prove this lemma, though we do need that fact to apply complete induction for the theorem overall.