proposition: Theorem setoid_fun_choice_imp_repr_fun_choice : SetoidFunctionalChoice -> RepresentativeFunctionalChoice .
proof: Proof. intros SetoidFunChoice A R Hequiv. apply SetoidFunChoice; firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts