proposition: Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice : FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice.
proof: Proof. intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists. assert (FunChoice : FunctionalChoice). { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice. - apply FunRelReify. - now apply repr_fun_choice_imp_relational_choice. } destruct (FunChoice _ _ T Hexists) as (f,Hf). destruct (ReprFunChoice A R Hequiv) as (g,Hg). exists (fun a => f (g a)). intro x. destruct (Hg x) as (Hgx,HRuniq). split. - eapply Hcompat. + symmetry. apply Hgx. + apply Hf. - intros y Hxy. f_equal. auto. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts