Library Choice

Definition choice A B :=
  ∀ (R:A->B->Prop),
  (∀ x:A, exists y:B, R x y) ->
  exists f:A->B, ∀ x:A, R x (f x).

Axiom choice_axiom : ∀ A B, choice A B.

Definition unique_choice A B (E:B->B->Prop) :=
  ∀ (R:A->B->Prop),
  (∀ x:A, exists y:B, R x y) ->
  (∀ x y y', R x y -> (R x y' <-> E y y')) ->
  exists f:A->B, ∀ x:A, R x (f x).