Library Choice
Axiom
choice
:
forall
(
A
B
:Type) (
R
:A->B->Prop),
(
forall
x
:A,
exists
y
:B,
R
x
y
) ->
exists
f
:A->B,
forall
x
:A,
R
x
(
f
x
).