proposition: Theorem setoid_fun_choice_imp_fun_choice : forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B.
proof: Proof. intros A B SetoidFunChoice T Hexists. destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf). - apply eq_equivalence. - now intros * ->. - assumption. - exists f. firstorder. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts