Let P be given.

Assume H1.

Let x, y and z be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hz: SNo z.

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.

We prove the intermediate claim LLz: ordinal (SNoLev z).

An exact proof term for the current goal is SNoLev_ordinal z Hz.

We prove the intermediate claim LsLz: ordinal (ordsucc (SNoLev z)).

An exact proof term for the current goal is ordinal_ordsucc (SNoLev z) LLz.

We prove the intermediate claim LzsLz: z ∈ SNoS_ (ordsucc (SNoLev z)).

An exact proof term for the current goal is SNoS_SNoLev z Hz.

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

∎