Let P be given.
Assume H1: ∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x.
We prove the intermediate claim L1: ∀α, ordinal α → ∀x ∈ SNoS_ α, P x.
Apply ordinal_ind to the current goal.
Let α be given.
Assume Ha: ordinal α.
Assume IH: ∀β ∈ α, ∀x ∈ SNoS_ β, P x.
Let x be given.
Assume Hx: x ∈ SNoS_ α.
Apply SNoS_E2 α Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ α.
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.
∎