Let t be given.
Assume Ht: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) t Ht).
∎