Introduction:  

* induction.v

Exercises:

* OneSortStackMachine.v and MultiSortStackMachine.v
* plist.v (parts a, b, c, d ,e)

OneSortStackMachine.v, MultiSortStackMachine.v come from
CPDT by Chlipala.