The Coq mailing list

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

> Well, I must prove that a certain transformation from a source  
> language to a
> target one preserves the semantics. "data_prop" refers to the type  
> of some
> objects the source language has. "data_prop" has the property  
> mentioned
> above and I thought that this should be reflected in the initial  
> definition
> and not given as a separate hypothesis.

It has been my experience that giving such definitions as separate  
hypothesis leads to much simpler proofs; but perhaps others will  
disagree with me completely :)

Edsko