The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

>   I don't understand what you mean by separating hypothesis. How would you
> separate the definitions if they are mutually recursive??

No, I wasn't referring to this. What I meant was that in my experience
it has been easier to work (for instance) a normal list and a hypothesis
with some property of the list, rather than try to encode a type of
lists that satisfy the property. Of course, this isn't a black-and-white
thing and for simple properties (vectors instead of lists is a good
example) the dependency improves proofs, so it varies from situation to
situation; but most of time I found it easier to separate the definition
of the data and its properties. 

Edsko