proposition: Lemma omniscient_fun_choice_imp_small_drinker : OmniscientFunctionalChoice -> SmallDrinker'sParadox.
proof: Proof. intros OAC_fun A P Inh. destruct (OAC_fun unit A (fun _ => P)) as (f,Hf). - auto. - exists (f tt); firstorder. Qed.
imports: RelationClasses Logic