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