proposition: Lemma independence_general_premises_drinker : IndependenceOfGeneralPremises <-> DrinkerParadox.
proof: Proof. split. - intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx. - intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx). exists x; intro HQ; apply (Hx (H HQ)). Qed.
imports: PropExtensionalityFacts Hurkens