An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ ∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0) f Hf).