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.
∎