Apply ordinal_ind to the current goal.

Let alpha be given.

Assume Ha: ordinal alpha.

Assume IH: ∀beta ∈ alpha, ∀z, SNo z → SNoLev z ∈ beta → P z.

Let z be given.

Assume Hz: SNo z.

Assume Hz2: SNoLev z ∈ alpha.

We will prove P z.

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

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

Apply SNo_etaE z Hz to the current goal.

Let L and R be given.

Assume H2: SNoCutP L R.

Assume H3: ∀x ∈ L, SNoLev x ∈ SNoLev z.

Assume H4: ∀y ∈ R, SNoLev y ∈ SNoLev z.

Assume H5: z = SNoCut L R.

Apply H2 to the current goal.

Assume H6.

Apply H6 to the current goal.

Assume H6: ∀x ∈ L, SNo x.

Assume H7: ∀y ∈ R, SNo y.

Assume H8: ∀x ∈ L, ∀y ∈ R, x < y.

rewrite the current goal using H5 (from left to right).

We will prove P (SNoCut L R).

Apply H1 to the current goal.

We will prove SNoCutP L R.

An exact proof term for the current goal is H2.

We will prove ∀x, x ∈ L → P x.

Let x be given.

Assume Hx: x ∈ L.

Apply IH (SNoLev z) Hz2 x to the current goal.

We will prove SNo x.

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

We will prove SNoLev x ∈ SNoLev z.

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

We will prove ∀y, y ∈ R → P y.

Let y be given.

Assume Hy: y ∈ R.

Apply IH (SNoLev z) Hz2 y to the current goal.

We will prove SNo y.

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

We will prove SNoLev y ∈ SNoLev z.

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