This file provides classical logic and unique choice; this is
weaker than providing iota operator and classical logic as the
definite descriptions provided by the axiom of unique choice can
be used only in a propositional context (especially, they cannot
be used to build functions outside the scope of a theorem proof)
Classical logic and unique choice, as shown in
[ChicliPottierSimpson02], implies the double-negation of
excluded-middle in
Set, hence it implies a strongly classical
world. Especially it conflicts with the impredicativity of
Set.
[ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
Simpson, Mathematical Quotients and Quotient Types in Coq,
Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
Springer Verlag.