The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Coq is believed to be consistent with the axiom [exists x, P x -> { x | P x }].

For the records, assuming I am parsing this correctly as [ (exists x, P x) -> { x | P x } ]. This is known to be inconsistent in general (you can use it to encode system U). It is a very strong property (because of impredicativity). See, Coquand's An Analysis of Girard's Paradox (LICS 1986).

/Arnaud