proposition: Theorem representative_choice : forall A (R:A->A->Prop), (Equivalence R) -> exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'.
proof: Proof. apply setoid_fun_choice_imp_repr_fun_choice. exact setoid_choice. Qed.
imports: ClassicalChoice ExtensionalFunctionRepresentative ChoiceFacts ClassicalFacts RelationClasses