coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?

From: Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>
To: Alexandre Miquel <miquel AT serveur-mail.lri.fr>
Cc: coq-club AT pauillac.inria.fr, Nicolas.Magaud AT sophia.inria.fr
Subject: Re: [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?
Date: Wed, 06 Nov 2002 12:07:20 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: LSV, ENS Cachan

Alexandre Miquel wrote:

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.

        What recent discovery?  Could you be more specific?
        Best,

        -- Jean Goubault-Larrecq, LSV, tel:+33-1 47 40 75 68.

[Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?, Nicolas Magaud
- <Possible follow-ups>
- [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?, Alexandre Miquel
  - Re: [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?, Jean Goubault-Larrecq