proposition: Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B.
proof: Proof. intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex. apply GenSetoidFunChoice; try easy. - apply eq_equivalence. - intros * H <-. firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts