Let n be given.

Assume Hn.

Apply SNoLtI2 0 (eps_ n) to the current goal.

We will prove SNoLev 0 ∈ SNoLev (eps_ n).

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

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

We will prove 0 ∈ ordsucc n.

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

We will prove SNoEq_ (SNoLev 0) 0 (eps_ n).

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

Let α be given.

Assume Ha: α ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE α Ha.

We will prove SNoLev 0 ∈ eps_ n.

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

We will prove 0 ∈ eps_ n.

We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎