proposition: Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox <-> OmniscientFunctionalChoice.
proof: Proof. intuition auto using omniscient_fun_choice_imp_small_drinker, omniscient_fun_choice_imp_fun_choice, fun_choice_and_small_drinker_imp_omniscient_fun_choice. Qed.
imports: RelationClasses Logic