Exercises:

* coqITP2015_course4.v
 (dependent pattern-matching, definitions using transparent type-cast)

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