Structural induction is a generalization of mathematical induction.
To see how, consider the definition of naturals (which mathematical induction is based on):
Inductive nat : Set := | O => nat | S => nat -> nat.
So, generally what we do is prove the base case , and then prove the recursive step by assuming .
Structural induction can be applied more generally, say lists.
Inductive natlist : Set := | nil => natlist | cons => nat -> natlist -> natlist.
In this case we prove the base case , and then prove the recursive step by assuming , where .
So as an example, let’s try to prove that .
First, let’s look at the definitions for map and id:
map _  =  map f (x:xs) = f x : map f xs id x = x
We use induction on x.
Inductive step: Assume that , and prove that .