Exercises:

* coqITP2015-course4.v
 (dependent pattern-mtching, definitions using transparent type-cast)

coqITP2015-course4.v comes from https://coq.inria.fr/coq-itp-2015