We will now introduce an induction principle for lists. It is derived directly from the definition of the list datatype.

**Induction Principle (Lists)**

*P* [] *P* (*t*)
=> *P* (*h* :: *t*)

forall

**Proposition (Interchange)**

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

**Exercise**

Prove by structural induction that for all 'a lists l1 and l2:length (l1 @ l2) = length l1 + length l2

**Proposition (Involution)**

The rev function is an involution, i.e. it always undoes its own work, since rev (rev l) = l.