We will prove {w ∈ SNoL 0|0 ≤ w} = 0.

rewrite the current goal using SNoL_0 (from left to right).

An exact proof term for the current goal is Sep_Empty (λw ⇒ 0 ≤ w).

∎