Let P be given.
Assume H1: ∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x.
We prove the intermediate claim L1: ∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, P x.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha: ordinal alpha.
Assume IH: ∀beta ∈ alpha, ∀x ∈ SNoS_ beta, P x.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Apply H1 x Hx3 to the current goal.
We will prove ∀w ∈ SNoS_ (SNoLev x), P w.
An exact proof term for the current goal is IH (SNoLev x) Hx1.
An exact proof term for the current goal is SNo_ordinal_ind P L1.
∎