Let x0 of type ι → ι → ο be given.
Apply ordinal_ind with
λ x1 . ∀ x2 . ordinal x2 ⟶ ∀ x3 . x3 ∈ SNoS_ x1 ⟶ ∀ x4 . x4 ∈ SNoS_ x2 ⟶ x0 x3 x4.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . ordinal x3 ⟶ ∀ x4 . x4 ∈ SNoS_ x2 ⟶ ∀ x5 . x5 ∈ SNoS_ x3 ⟶ x0 x4 x5.
Apply ordinal_ind with
λ x2 . ∀ x3 . x3 ∈ SNoS_ x1 ⟶ ∀ x4 . x4 ∈ SNoS_ x2 ⟶ x0 x3 x4.
Let x2 of type ι be given.
Assume H4:
∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ SNoS_ x1 ⟶ ∀ x5 . x5 ∈ SNoS_ x3 ⟶ x0 x4 x5.
Let x3 of type ι be given.
Assume H5:
x3 ∈ SNoS_ x1.
Let x4 of type ι be given.
Assume H6:
x4 ∈ SNoS_ x2.
Apply SNoS_E2 with
x1,
x3,
x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply SNoS_E2 with
x2,
x4,
x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply H0 with
x3,
x4 leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H13.
Let x5 of type ι be given.
Apply H2 with
SNoLev x3,
x2,
x5,
x4 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
Apply H4 with
SNoLev x4,
x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply H2 with
SNoLev x3,
SNoLev x4,
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H12.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply SNo_ordinal_ind2 with
x0.
The subproof is completed by applying L1.