Pattern-matching dependent types in Coq

Code from a talk given at YOW! Lambda Jam 2015. You'll probably be more interested in the process of writing this code, in which case you should go watch the video.