Let x, A and B be given.

Assume HAB: A = B.

Assume Hx: x ∈ B.

We will prove x ∈ A.

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

An exact proof term for the current goal is Hx.

∎