Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x1 = x0.
Apply SNoLev_prop with
x0,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoS_E2 with
SNoLev x0,
x1,
False leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply In_irref with
SNoLev x1.
Apply H2 with
λ x2 x3 . SNoLev x1 ∈ SNoLev x3.
The subproof is completed by applying H5.