Let x be given.
Assume Hx1 Hx2.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal x Hx1 to the current goal.
Assume Hx1a Hx1b Hx1c Hx1d.
Apply SNoLtE x ω Hx1c SNo_omega Hx2 to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev ω.
Assume Hz3: SNoEq_ (SNoLev z) z x.
Assume Hz4: SNoEq_ (SNoLev z) z ω.
Assume Hz5: x < z.
Assume Hz6: z < ω.
Assume Hz7: SNoLev z ∉ x.
Assume Hz8: SNoLev z ∈ ω.
We prove the intermediate claim Lz1: ordinal (SNoLev z).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hz1.
We prove the intermediate claim Lz2: SNo (SNoLev z).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lz1.
We use (SNoLev z) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz8.
We will prove x < SNoLev z.
Apply SNoLtLe_tra x z (SNoLev z) Hx1c Hz1 Lz2 Hz5 to the current goal.
We will prove z ≤ SNoLev z.
Apply ordinal_SNoLev_max_2 (SNoLev z) Lz1 z Hz1 to the current goal.
We will prove SNoLev z ∈ ordsucc (SNoLev z).
Apply ordsuccI2 to the current goal.
Assume H1: SNoLev x ∈ SNoLev ω.
Assume H2: SNoEq_ (SNoLev x) x ω.
Assume H3: SNoLev x ∈ ω.
We prove the intermediate claim Lx1: ordinal (SNoLev x).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx1c.
We prove the intermediate claim Lx2: ordinal (ordsucc (SNoLev x)).
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Lx1.
We use (ordsucc (SNoLev x)) to witness the existential quantifier.
Apply andI to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is H3.
We will prove x < ordsucc (SNoLev x).
Apply ordinal_SNoLev_max (ordsucc (SNoLev x)) Lx2 x Hx1c to the current goal.
We will prove SNoLev x ∈ ordsucc (SNoLev x).
Apply ordsuccI2 to the current goal.
rewrite the current goal using ordinal_SNoLev ω omega_ordinal (from left to right).
Assume H1: ω ∈ SNoLev x.
We will prove False.
Apply ordsuccE ω (SNoLev x) Hx1a to the current goal.
Assume H2: SNoLev x ∈ ω.
An exact proof term for the current goal is In_no2cycle (SNoLev x) ω H2 H1.
Assume H2: SNoLev x = ω.
Apply In_irref ω to the current goal.
rewrite the current goal using H2 (from right to left) at position 2.
An exact proof term for the current goal is H1.
∎