proposition: Lemma excluded_middle_independence_general_premises : generalized_excluded_middle -> DrinkerParadox.
proof: Proof. intros GEM A P x0. destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot]. - exists x; intro; exact Hx. - exists x0; exact Hnot. Qed.
imports: PropExtensionalityFacts Hurkens