Let x be given.
Assume Hx.
Apply set_ext to the current goal.
We will prove SNoLev (- x) ⊆ SNoLev x.
An exact proof term for the current goal is minus_SNo_Lev_lem2 x Hx.
We will prove SNoLev x ⊆ SNoLev (- x).
rewrite the current goal using minus_SNo_invol x Hx (from right to left) at position 1.
We will prove SNoLev (- - x) ⊆ SNoLev (- x).
An exact proof term for the current goal is minus_SNo_Lev_lem2 (- x) (SNo_minus_SNo x Hx).
∎