Proving property of a term using Induction

This is one of the example lemma that has been proved in TAPL
book which I'm unable to grasp.

The objective is to prove |Consts(t)| <= size(t) where t is a term.

Now, Consts is a function defined like this:

Consts(true) = {true}
Consts(false) = {false}
... and so on

Similarly

size(true) = 1
size(false) = 1
... and so on

Now the proof in the book starts with something like "By
induction on the depth of t" and then goes to prove the
lemma. But I think I'm missing something here. Induction can be
applied when we have to prove something over natural number. But
there is no natural number involved in the above lemma. How come
then the induction is applied ?

A term is defined recursively. You can do induction on recursive types, using structural induction.

For instance, suppose we say that a term is something of the form

-
$c$ (a constant), or

-
$t_1+t_2$, where $t_1,t_2$ are terms.

Then structural induction is (loosely) similar to doing a proof by (strong) induction on the size of the tree. You prove that the property holds if the term has the form $c$ (that's the base case). Then, you prove that if the property holds for terms $t_1$ and $t_2$, then the property holds for the term $t_1+t_2$. You can probably see how to generalize this to terms whose syntax has a more complicated definition.

StackExchange Computer Science Q#70586, answer score: 4