proposition: Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice : FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox -> OmniscientFunctionalChoice.
proof: Proof. intros AC_fun Drinker A B R Inh. destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf). - intro x; apply (Drinker B (R x) Inh). - exists f; assumption. Qed.
imports: RelationClasses Logic