Let P be given.

Assume H1.

Let x be given.

Assume Hx: SNo x.

We prove the intermediate claim LLx: ordinal (SNoLev x).

An exact proof term for the current goal is SNoLev_ordinal x Hx.

We prove the intermediate claim LsLx: ordinal (ordsucc (SNoLev x)).

An exact proof term for the current goal is ordinal_ordsucc (SNoLev x) LLx.

We prove the intermediate claim LxsLx: x ∈ SNoS_ (ordsucc (SNoLev x)).

An exact proof term for the current goal is SNoS_SNoLev x Hx.

An exact proof term for the current goal is H1 (ordsucc (SNoLev x)) LsLx x LxsLx.

∎