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