proposition: Lemma omniscient_fun_choice_imp_fun_choice : OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
proof: Proof. intros OAC_fun A B Inh R H. destruct (OAC_fun A B R Inh) as (f,Hf). exists f; firstorder. Qed.
imports: RelationClasses Logic