An exact proof term for the current goal is (λX Y z H ⇒ SepE X (λx : set ⇒ x ∉ Y) z H).