The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi Adam,

On Mon, Mar 01, 2010 at 09:47:31PM +0100, Adam Koprowski wrote:
> 
>   A quick answer would be: take a look at the proof-irrelevance axiom
> (Coq.Logic.ProofIrrelevance), which will allow you to equate such
> obligations.

Thanks, but how do I actually tell coq to apply it to the right places?

I'd rather not have to write out
    assert (EnlargeTransitiveCommuteRelation2_obligation_4 ... =
            EnlargeTransitiveCommuteRelation2_obligation_1 ...).
        apply proof_irrelevance.
etc. if I can get away without it.


Thanks
Ian