Library Coq.Logic.RelationalChoice

This file axiomatizes the relational form of the axiom of choice





Axiom relational_choice :

  forall (A B : Type) (R : A->B->Prop),

   (forall x : A, exists y : B, R x y) ->

     exists R' : A->B->Prop, 

       subrelation R' R /\ forall x : A, exists! y : B, R' x y.