We will prove {w ∈ SNoL 1|0 ≤ w} = 1.
rewrite the current goal using SNoL_1 (from left to right).
We will prove {w ∈ 1|0 ≤ w} = 1.
Apply set_ext to the current goal.
An exact proof term for the current goal is Sep_Subq 1 (λw ⇒ 0 ≤ w).
Let w be given.
Assume Hw: w ∈ 1.
Apply cases_1 w Hw to the current goal.
We will prove 0 ∈ {w ∈ 1|0 ≤ w}.
Apply SepI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
∎