Let x, y and S be given.

Assume Hxy: x = y.

Assume HyS: y ∈ S.

We will prove x ∈ S.

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

An exact proof term for the current goal is HyS.

∎