Let x be given.
Assume Hx: SNo x.
Assume H2: ∀y ∈ SNoS_ (SNoLev x), y < x.
We prove the intermediate claim LLx1: ordinal (SNoLev x).
An exact proof term for the current goal is SNoLev_ordinal x Hx.
We prove the intermediate claim LLx2: SNo (SNoLev x).
An exact proof term for the current goal is ordinal_SNo (SNoLev x) LLx1.
We prove the intermediate claim L3: x ≤ SNoLev x.
Apply ordinal_SNoLev_max_2 (SNoLev x) LLx1 x Hx to the current goal.
We will prove SNoLev x ∈ ordsucc (SNoLev x).
Apply ordsuccI2 to the current goal.
Apply SNoLeE x (SNoLev x) Hx LLx2 L3 to the current goal.
Assume H3: x < SNoLev x.
We will prove False.
Apply SNoLtE x (SNoLev x) Hx LLx2 H3 to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev x ∩ SNoLev (SNoLev x).
Assume Hz2: SNoEq_ (SNoLev z) z x.
Assume Hz3: SNoEq_ (SNoLev z) z (SNoLev x).
Assume Hz4: x < z.
Assume Hz5: z < SNoLev x.
Assume Hz6: SNoLev z ∉ x.
Assume Hz7: SNoLev z ∈ SNoLev x.
Apply SNoLt_irref z to the current goal.
Apply SNoLt_tra z x z Hz Hx Hz to the current goal.
We will prove z < x.
Apply H2 to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
Apply SNoS_I (SNoLev x) LLx1 z (SNoLev z) to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hz7.
We will prove SNo_ (SNoLev z) z.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hz.
We will prove x < z.
An exact proof term for the current goal is Hz4.
Assume H4: SNoLev x ∈ SNoLev (SNoLev x).
We will prove False.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using ordinal_SNoLev (SNoLev x) LLx1 (from right to left) at position 2.
An exact proof term for the current goal is H4.
Assume H4: SNoLev (SNoLev x) ∈ SNoLev x.
We will prove False.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using ordinal_SNoLev (SNoLev x) LLx1 (from right to left) at position 1.
An exact proof term for the current goal is H4.
Assume H3: x = SNoLev x.
Use symmetry.
An exact proof term for the current goal is H3.
∎