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