proposition: Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B.
proof: Proof. intros A B SetoidFunChoice R T Hequiv Hexists. pose (T' x y := forall x', R x x' -> T x' y). assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder. destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf). exists f. firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts