Exercises:

* coqITP2015_course4.v
 (dependent pattern-matching, definitions using transparent type-cast)
 - part after *** END LECTURE ****
 - vector_eta, Vcons_inj (more difficult) 

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