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