Let x, y and S be given.

Assume Hxy: x = y.

Assume HxS: x ∈ S.

We will prove y ∈ S.

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

An exact proof term for the current goal is HxS.

∎