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