An exact proof term for the current goal is (λX Y z H1 H2 ⇒ SepI X (λx : set ⇒ x ∈ Y) z H1 H2).