The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Pierre Castéran wrote:
>   I didn't find which command would allow me to find the differences
> between the two occurrences of the term "Edges.mem (phi x, a) (E_of G') "

Try:

Set Printing Implicit.
Unset Printing Notations.

I think this is enough to show you the exact representations of terms.  
I have also found it to be true that 'rewrite' needs representations to 
match exactly and won't consider definitional equality, so this seems 
like a good way to find the problem.