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