An exact proof term for the current goal is (λX P x H ⇒ SepE X P x H (x ∈ X) (λH _ ⇒ H)).