An exact proof term for the current goal is (Eps_i_ex (λf : set ⇒ f ∈ C_I_R) C_I_R_nonempty).