The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 13/12/2013 00:30, Daniel Schepler wrote:
> The Extensionality_Ensembles axiom in
> http://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html
> easily implies propositional extensionality

In a similar way, propositional extensionality was used to prove the 
consistency of the set theory of Why3. And my email would be incomplete 
if I didn't quote the comment accompanying that Coq proof: "it is 
folklore that the two together are consistent". Famous last words...

Best regards,

Guillaume