The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

The Extensionality_Ensembles axiom in http://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html easily implies propositional extensionality; and I know I used Extensionality_Ensembles a lot in my ZornsLemma and Topology contributions.
--

Daniel Schepler

On Thu, Dec 12, 2013 at 3:23 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 12/12/2013 22:41, Maxime Dénès wrote:
> Arthur and I refined Daniel's example to show that Propositional
> Extensionality (even the weaker version of it) as defined in Coq's
> standard library is inconsistent in Coq's current theory:

That's really surprising, to say the least... Is there a lot of
contributions using this axiom in the wild?

PMP