proposition: Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B.
proof: Proof. intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists. destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts