Let P and x be given.

Assume Hx: P x.

Assume Huniq: ∀y : set, P y → y = x.

We will prove Eps_i P = x.

We prove the intermediate claim HE: P (Eps_i P).

An exact proof term for the current goal is (Eps_i_ax P x Hx).

An exact proof term for the current goal is (Huniq (Eps_i P) HE).

∎