Let x0 of type ι be given.
Apply set_ext with
SNoLev (minus_SNo x0),
SNoLev x0 leaving 2 subgoals.
Apply minus_SNo_Lev_lem2 with
x0.
The subproof is completed by applying H0.
Apply minus_SNo_invol with
x0,
λ x1 x2 . SNoLev x1 ⊆ SNoLev (minus_SNo x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply minus_SNo_Lev_lem2 with
minus_SNo x0.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H0.