apply in expression

Stream: general

[Sebastien Gouezel]

Is there a way to apply in the middle of an expression? Let me explain. Assume that lemma foo tells me that Q can be deduced from P. Now, I have in the middle of a proof a goal of the form ∀x, Q x, and I would like to reduce it to ∀x, P x without introducing x. Just like simp would do instead of rw, but for implications instead of equivalences. Is this possible?