Let x be given.

Assume Hx.

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 Subq_finite (SNoS_ (SNoLev x)) to the current goal.

We will prove finite (SNoS_ (SNoLev x)).

An exact proof term for the current goal is SNoS_finite (SNoLev x) Hx1.

We will prove SNoL x ⊆ SNoS_ (SNoLev x).

Let y be given.

Assume Hy.

Apply SNoL_E x Hx3 y Hy to the current goal.

Assume Hy1 Hy2 Hy3.

We will prove y ∈ SNoS_ (SNoLev x).

Apply SNoS_I2 y x ?? ?? to the current goal.

We will prove SNoLev y ∈ SNoLev x.

An exact proof term for the current goal is Hy2.

∎