We will prove unit_interval_left_half ∪ unit_interval_right_half = unit_interval.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ unit_interval_left_half ∪ unit_interval_right_half.
We will prove t ∈ unit_interval.
Apply (binunionE unit_interval_left_half unit_interval_right_half t Ht) to the current goal.
Assume HtL: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtL).
Assume HtR: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtR).
Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove t ∈ unit_interval_left_half ∪ unit_interval_right_half.
Apply (xm (Rlt t (eps_ 1))) to the current goal.
Assume Htlt: Rlt t (eps_ 1).
We prove the intermediate claim Hnlt: ¬ (Rlt (eps_ 1) t).
An exact proof term for the current goal is (not_Rlt_sym t (eps_ 1) Htlt).
We prove the intermediate claim HtL: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) t HtI Hnlt).
An exact proof term for the current goal is (binunionI1 unit_interval_left_half unit_interval_right_half t HtL).
Assume Hnlt: ¬ (Rlt t (eps_ 1)).
We prove the intermediate claim HtR: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) t HtI Hnlt).
An exact proof term for the current goal is (binunionI2 unit_interval_left_half unit_interval_right_half t HtR).
∎