Let x be given.

Assume Hx.

Let w be given.

Assume Hw1 Hw2.

Apply real_E x Hx to the current goal.

Assume Hx1: SNo x.

Assume Hx2: SNoLev x ∈ ordsucc ω.

Assume _ _ _ _ _.

We prove the intermediate claim L1: SNoLev w ∈ ω.

Apply ordsuccE ω (SNoLev x) Hx2 to the current goal.

Assume H1: SNoLev x ∈ ω.

An exact proof term for the current goal is omega_TransSet (SNoLev x) H1 (SNoLev w) Hw2.

Assume H1: SNoLev x = ω.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is Hw2.

Apply SNoS_I ω omega_ordinal w (SNoLev w) L1 to the current goal.

We will prove SNo_ (SNoLev w) w.

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is Hw1.

∎