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