noob "resuse variable name" question

Stream: general

[Kevin Buzzard]

Dammit I can never remember how to go from H : P and HPQ : P -> Q to H : Q in tactic mode, the point being that I want to throw the original H away and reuse the name. There's a tactic that does this but I can never remember the name and I can't come up with an algorithm to find out for myself, my searches have been futile, so sorry, I have to ask.

[Chris Hughes]

specialize or replace

[Kevin Buzzard]

replace -- that was it. I knew it was something like rewrite. Thanks.