Let n be given.
Assume Hn: n ∈ ω.
Apply SNoS_I ω omega_ordinal n n to the current goal.
An exact proof term for the current goal is Hn.
We will prove SNo_ n n.
rewrite the current goal using ordinal_SNoLev n (nat_p_ordinal n (omega_nat_p n Hn)) (from right to left) at position 1.
We will prove SNo_ (SNoLev n) n.
Apply SNoLev_ to the current goal.
Apply omega_SNo to the current goal.
An exact proof term for the current goal is Hn.
∎