This is one of the example lemma that has been proved in TAPLbook 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 onSimilarlysize(true) = 1size(false) = 1... and so onNow the proof in the book starts with something like Byinduction on the depth of t and then goes to prove thelemma. But I think I'm missing something here. Induction can beapplied when we have to prove something over natural number. Butthere is no natural number involved in the above lemma. How comethen the induction is applied ?
Proving property of a term using Induction
type theory;induction