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.
pose proof (H x) as H'.
The parentheses are optional.