Let n be given.

Assume Hn.

Apply SNoS_I ω omega_ordinal (eps_ n) (ordsucc n) to the current goal.

We will prove ordsucc n ∈ ω.

An exact proof term for the current goal is omega_ordsucc n Hn.

We will prove SNo_ (ordsucc n) (eps_ n).

An exact proof term for the current goal is SNo__eps_ n Hn.

∎