Let x and U be given.

Assume HxU.

We will prove {x} ⊆ U.

Let y be given.

Assume Hy: y ∈ {x}.

We will prove y ∈ U.

We prove the intermediate claim HyEq: y = x.

An exact proof term for the current goal is (SingE x y Hy).

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

An exact proof term for the current goal is HxU.

∎