The [convoy pattern](http://adam.chlipala.net/cpdt/html/MoreDep.html) is invaluable for writing functions over dependent types. It would be nice to have a good example of it here too.