The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 02/24/2012 05:07 AM, Pierre Courtieu wrote:
> Hello, here is a script proving your goal in v8.3 and v8.4 (14975). It
> makes use of JMeq but the statement of the lemma is the one you want.
>    

But the original request asked for an axiom-free proof, right?  Your 
proof uses axiom [JMeq_eq].