coq tactic - How to introduce a new existential condition from a witness in Coq? -

my question relates how construct exist term in set of conditions/hypotheses.

i have following intermediate proof state:

x : type p : x -> prop h : (exists x : x, p x -> false) -> false x : x h0 : p x -> false ______________________________________(1/1) p x 

in mind, know because of h0, x witness (exists x : x, p x -> false), , want introduce name:

w: (exists x : x, p x -> false) 

based on above reasoning , use apply h in w generate false in hypothesis, , inversion false.

but don't know tactic/syntax use introduce witness w above. best can reach far check (ex_intro _ (fun x => p x -> false) x h0)). gives false.

can explain how introduce existential condition, or alternative way finish proof?

thanks.

p.s. have whole theorem prove is:

theorem not_exists_dist :   excluded_middle ->   forall (x:type) (p : x -> prop),     ~ (exists x, ~ p x) -> (forall x, p x). proof.   unfold excluded_middle. unfold not.    intros exm x p h x.    destruct (exm (p x)).     apply h0.     check (h (ex_intro _ (fun x => p x -> false)  x h0)). 

here, since know how construct term of type false, can add context using pose proof. gives:

pose proof (h (ex_intro (fun x => p x -> false)  x h0)) 

you can directly destruct term, solves goal.

destruct (h (ex_intro (fun x => p x -> false)  x h0)) 

another way finish proof prove false. can change goal false tactics exfalso or contradiction. approach, can use hypotheses of form _ -> false otherwise difficult manipulate. proof, can write:

exfalso. apply h. (* or directly, contradiction h *) exists x. assumption.