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

An exact proof term for the current goal is ordinal_SNo (SNoLev x) LLx1.

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.

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