proposition: Theorem setoid_choice : forall A B, forall R : A -> A -> Prop, forall T : A -> B -> Prop, Equivalence R -> (forall x x' y, R x x' -> T x y -> T x' y) -> (forall x, exists y, T x y) -> exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x').
proof: Proof. apply setoid_functional_choice_first_characterization. split; [|split]. - exact choice. - exact extensional_function_representative. - exact classic. Qed.
imports: ClassicalChoice ExtensionalFunctionRepresentative ChoiceFacts ClassicalFacts RelationClasses