Exercises:

* plist.v (part f)
* coqITP2015_ex4_tuple.v

plist.v comes from CPDT by Chlipala.
coqITP2015_ex4_tuple.v comes from https://coq.inria.fr/coq-itp-2015