An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) t Ht).