We will now introduce an induction principle for lists. It is derived directly from the definition of the list datatype.
Induction Principle (Lists)
The rev function and the append operator obey an interchange law since the following holds for all 'a lists l1 and l2.
rev (l1 @ l2) = rev l2 @ rev l1
Prove by structural induction that for all 'a lists l1 and l2:
length (l1 @ l2) = length l1 + length l2
The rev function is an involution, i.e. it always undoes its own work, since rev (rev l) = l.