The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Suppose you have a constructive proof of a statement "there is an x
satisfying P":

  exists x : A, P x

Then your proof contains an actual construction of such an x. Instead
of having proved the above statement, you should have constructed an
element of the set

  {x : A | P x}

You can throw in uniqueness if you want, but it does not add much in
terms of conceptual understanding.

If you existence proof is not constructive, you should make it constructive.

If it is not possible to make it constructive, you should change your theory.

If you don't want to change your theory, then you can assume the
definite description axiom that Christian Doczkal mentioned. In fact,
what many people do not realize is that some form of such an axiom is
needed in classical mathematics, too.

With kind regards,

Andrej