proposition: Theorem setoid_fun_choice_imp_gen_setoid_fun_choice : forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B.
proof: Proof. intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex. destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy. { intros; apply (Hcompat x x' y y); try easy. } exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts