(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                drinker.v                                 *)
(****************************************************************************)


Theorem drinker's_theorem :
 (forall P : Prop, P \/ ~ P) ->
 forall (U : Set) (x : U) (Q : U -> Prop),
 exists x : U, Q x -> forall x : U, Q x.
(* Goal: forall (_ : forall P : Prop, or P (not P)) (U : Set) (_ : U) (Q : forall _ : U, Prop), @ex U (fun x0 : U => forall (_ : Q x0) (x1 : U), Q x1) *)
intros Excluded_middle U x Q.
generalize (Excluded_middle (exists x : U, ~ Q x)); intro h; elim h; intro H';
 clear h.
(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
elim H'; intros z E; clear H'.
(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
exists z; intro H'0.
(* Goal: forall x : U, Q x *)
(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
elim E; assumption.

(* Goal: @ex U (fun x : U => forall (_ : Q x) (x0 : U), Q x0) *)
exists x; intros H'0 x0.
generalize (Excluded_middle (Q x0)); intro h; elim h; intro H'1; clear h;
 auto.
(* Goal: Q x0 *)
elim H'; exists x0; assumption.
Qed.