Let x be given.

Assume Hx: SNo x.

An exact proof term for the current goal is Eps_i_ex (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) Hx.

∎