Tactic to unify with hypothesis

Stream: general

[Miguel Marco]

Does there exists a tactic that, given a hypothesis P a and a target P b allows one to change it to a = b?

I know I could add the extra hypothesis a = b and prove it, but in my case a is a quite complicated expression that is not easy to reproduce right away.

[Jireh Loreaux]

Sorry, I mean convert h where h : P a. If it's too eager, you can tame it with convert h using 37 where 37 is generally 0,1,2,3,4.

[Jireh Loreaux]

(deleted)