2

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.

Community
  • 1
  • 1
user287393
  • 1,221
  • 8
  • 13

3 Answers3

5

pose proof (H x) as H'.

The parentheses are optional.

Ptival
  • 9,167
  • 36
  • 53
3

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).
max taldykin
  • 12,459
  • 5
  • 45
  • 64
1

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.

Virgile
  • 9,724
  • 18
  • 42