Let n be given.

Assume Hn.

Set L to be the term {0}.

Set R to be the term {eps_ m|m ∈ n}.

We prove the intermediate claim Ln: nat_p n.

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

We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).

Apply and3I to the current goal.

Let w be given.

Assume Hw.

rewrite the current goal using SingE 0 w Hw (from left to right).

An exact proof term for the current goal is SNo_0.

Let z be given.

Assume Hz.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

Assume Hm1: m ∈ n.

Assume Hm2: z = eps_ m.

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

Apply SNo_eps_ to the current goal.

We will prove m ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_p_trans n Ln m Hm1.