An exact proof term for the current goal is nat_p_omega n Hn.

Assume H2: x < eps_ n.

We will prove False.

Apply SNoLtE x (eps_ n) Hx3 (SNo_eps_ n Ln) H2 to the current goal.

Let z be given.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev (eps_ n).

Assume Hz3: SNoEq_ (SNoLev z) z x.

Assume Hz4: SNoEq_ (SNoLev z) z (eps_ n).

Assume Hz5: x < z.

Assume Hz6: z < eps_ n.

Assume Hz7: SNoLev z ∉ x.

Assume Hz8: SNoLev z ∈ eps_ n.

We prove the intermediate claim Lz0: z = 0.

Apply SNoLev_0_eq_0 z Hz1 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev z) (SNoLev_ordinal z Hz1) Hz8.

Apply SNoLt_irref x to the current goal.

We will prove x < x.

Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.

We will prove z < x.

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

An exact proof term for the current goal is Hxpos.

Assume H1: SNoLev x ∈ SNoLev (eps_ n).

Assume H2: SNoEq_ (SNoLev x) x (eps_ n).

Assume H3: SNoLev x ∈ (eps_ n).

We prove the intermediate claim Lx0: x = 0.

Apply SNoLev_0_eq_0 x Hx3 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev x) Hx2 H3.

Apply SNoLt_irref x to the current goal.

rewrite the current goal using Lx0 (from left to right) at position 1.

An exact proof term for the current goal is Hxpos.

rewrite the current goal using SNoLev_eps_ n Ln (from left to right).

Assume H3: ordsucc n ∈ SNoLev x.

We will prove False.

Apply ordsuccE (ordsucc n) (SNoLev x) Hx1 to the current goal.

Assume H4: SNoLev x ∈ ordsucc n.

An exact proof term for the current goal is In_no2cycle (SNoLev x) (ordsucc n) H4 H3.

Assume H4: SNoLev x = ordsucc n.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using H4 (from left to right) at position 1.

An exact proof term for the current goal is H3.

Assume H2: eps_ n ≤ x.

An exact proof term for the current goal is H2.