An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ ¬ (Rlt b x0)) x Hx).