Let x0 of type ι be given.
Apply SNoLev_ordinal with
x0.
The subproof is completed by applying H0.
Apply ordinal_SNo with
SNoLev x0.
The subproof is completed by applying L2.
Apply ordinal_SNoLev_max_2 with
SNoLev x0,
x0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
The subproof is completed by applying ordsuccI2 with
SNoLev x0.
Apply SNoLeE with
x0,
SNoLev x0,
SNoLev x0 = x0 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply FalseE with
SNoLev x0 = x0.
Apply SNoLtE with
x0,
SNoLev x0,
False leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply SNoLt_irref with
x1.
Apply SNoLt_tra with
x1,
x0,
x1 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
Apply H1 with
x1.
Apply SNoS_I with
SNoLev x0,
x1,
SNoLev x1 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H13.
Apply SNoLev_ with
x1.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply FalseE with
SNoEq_ (SNoLev x0) x0 (SNoLev x0) ⟶ SNoLev x0 ∈ SNoLev x0 ⟶ False.
Apply In_irref with
SNoLev x0.
Apply ordinal_SNoLev with
SNoLev x0,
λ x1 x2 . SNoLev x0 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H5 with λ x2 x3 . x1 x3 x2.