Library Coq.Logic.IndefiniteDescription
This file provides a constructive form of indefinite description that
allows to build choice functions; this is weaker than Hilbert's
epsilon operator (which implies weakly classical properties) but
stronger than the axiom of choice (which cannot be used outside
the context of a theorem proof).