Let x0 of type ι → ι → ι → ο be given.
Apply ordinal_ind with
λ x1 . ∀ x2 . ordinal x2 ⟶ ∀ x3 . ordinal x3 ⟶ ∀ x4 . x4 ∈ SNoS_ x1 ⟶ ∀ x5 . x5 ∈ SNoS_ x2 ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ x0 x4 x5 x6.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . ordinal x3 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 . x5 ∈ SNoS_ x2 ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ ∀ x7 . x7 ∈ SNoS_ x4 ⟶ x0 x5 x6 x7.
Apply ordinal_ind with
λ x2 . ∀ x3 . ordinal x3 ⟶ ∀ x4 . x4 ∈ SNoS_ x1 ⟶ ∀ x5 . x5 ∈ SNoS_ x2 ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ x0 x4 x5 x6.
Let x2 of type ι be given.
Assume H4:
∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 . x5 ∈ SNoS_ x1 ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ ∀ x7 . x7 ∈ SNoS_ x4 ⟶ x0 x5 x6 x7.
Apply ordinal_ind with
λ x3 . ∀ x4 . ... ⟶ ∀ x5 . x5 ∈ ... ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ x0 x4 x5 x6.
Apply SNo_ordinal_ind3 with
x0.
The subproof is completed by applying L1.