Let w be given.

Assume Hw: SNo w.

Let x be given.

Assume Hx: x ∈ SNoS_ (SNoLev w).

Assume Hxw: x = w.

Apply SNoLev_prop w Hw to the current goal.

Assume Hw1: ordinal (SNoLev w).

Assume Hw2: SNo_ (SNoLev w) w.

Apply SNoS_E2 (SNoLev w) Hw1 x Hx to the current goal.

Assume Hx1: SNoLev x ∈ SNoLev w.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We will prove False.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using Hxw (from left to right) at position 2.

An exact proof term for the current goal is Hx1.

∎