Let x0 of type ι be given.
Apply SNoLev_prop with
x0,
x0 ∈ SNoS_ (ordsucc (SNoLev x0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoS_I with
ordsucc (SNoLev x0),
x0,
SNoLev x0 leaving 3 subgoals.
Apply ordinal_ordsucc with
SNoLev x0.
The subproof is completed by applying H1.
The subproof is completed by applying ordsuccI2 with
SNoLev x0.
The subproof is completed by applying H2.