Let x be given.
Assume Hx: x ∈ SNoS_ ω.
Apply SNoS_E2 ω omega_ordinal 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 SNoS_omega_diadic_rational_p_lem (SNoLev x) to the current goal.
We will prove nat_p (SNoLev x).
An exact proof term for the current goal is omega_nat_p (SNoLev x) Hx1.
We will prove SNo x.
An exact proof term for the current goal is Hx3.
We will prove SNoLev x = SNoLev x.
Use reflexivity.
∎