proposition: Corollary setoid_fun_choice_imp_functional_rel_reification : forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B.
proof: Proof. intros A B SetoidFunChoice. apply fun_choice_imp_functional_rel_reification. now apply setoid_fun_choice_imp_fun_choice. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts