The Coq mailing list

[Alexandre Miquel <miquel AT serveur-mail.lri.fr>]

> In a word: I would like to know whether I can safely add the
> following axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)
> in the Coq system.

Yes, it is safe.

Of course, due to the recent discovery of Laurent Chicli, Loic Pottier
and Carlos Simpson, I have to give some degree of confidence in
my statement, to protect myself against earthquakes.

Confidence is quite high for this result (which is trivial if we
consider Coq without Set), since both models of the system that
include Set validate this axiom (provided this axiom is stated in
Prop, of course).

And you can easily check that your axiom entails proof-irrelevance
too.  (It was part of the subject of the exam of the CIC course - DEA
Programmation, in 1999.)

But, as mentioned by Carlos, are you *really* sure you want to
add this?

-- Alexandre Miquel