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).