proposition: Theorem repr_fun_choice_imp_ext_function_repr : RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative.
proof: Proof. intros ReprFunChoice A B. pose (R (f g : A -> B) := forall x : A, f x = g x). assert (Hequiv:Equivalence R). { split; try easy. firstorder using eq_trans. } apply (ReprFunChoice _ R Hequiv). Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts