Let x, A and B be given.

Assume HAB: A = B.

Assume Hx: x ∈ A.

We will prove x ∈ B.

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

An exact proof term for the current goal is Hx.

∎