Let x, y and z be given.

Assume H1 H2.

rewrite the current goal using H2 (from right to left).

An exact proof term for the current goal is H1.

∎