The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

It's possible that there are some issues specific to your problem that 
deserve discussion on this list, but my recommendation is to read some 
parts of CPDT that discuss programming with dependent types:
    http://adam.chlipala.net/cpdt/
I expect Chapter 7 is the most relevant, as I see your code contains 
some of the mistakes described there.  Really, of course, I recommend 
the whole book up to Part III for anyone who wants to put Coq to work. ;)