Variable Klub: Set.
Variable boit: Klub->Prop.
Variable gege: Klub.

Axiom te : forall P: Prop, P\/~P.

Axiom nonnon: forall P: Prop, ~~P->P.

Theorem drinkers: exists x, boit x -> forall y, boit y.

destruct te with (P:=exists x, ~ boit x).

destruct H.
exists x.
intros.
destruct H.
apply H0.

exists gege.
intros.

(* apply nonnon. intro. destruct H. exists y. apply H1. *)

destruct te with (P:=(boit y)).
apply H1.
destruct H.
exists y.
apply H1.

Qed.