Let P be given.

Assume H1.

Let x and y be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

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.

We prove the intermediate claim LLy: ordinal (SNoLev y).

An exact proof term for the current goal is SNoLev_ordinal y Hy.

We prove the intermediate claim LsLy: ordinal (ordsucc (SNoLev y)).

An exact proof term for the current goal is ordinal_ordsucc (SNoLev y) LLy.

We prove the intermediate claim LysLy: y ∈ SNoS_ (ordsucc (SNoLev y)).

An exact proof term for the current goal is SNoS_SNoLev y Hy.

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

∎