Best way to perform universal instantiation in Coq

Question

Suppose I have an hypothesis H : forall ( x : X ), P x and a variable x : X in the context. I want to perform universal instantiation and obtain a new hypothesis H' : P x. What is the most painless way to do this? Apparently apply H in x does not work. assert ( P x ) followed by apply H does, but it can get very messy if P is complex.

There's a similar question that seems somewhat related. Not sure if it can be applied here, though.

Answer 1

pose proof (H x) as H'.

The parentheses are optional.

Answer 2

If you want new hypothesis you can use @Ptival's answer, or

assert (H' := H x).

If it is ok to substitute existing hypothesis

specialize (H x).

Answer 3

You can use something like generalize (H x); intros Hx: generalize will add (H x) as a new implication in front of the current goal, and intros will put it in your hypotheses.