Let x be given.

Assume Hx: x ∈ SNoL 1.

We will prove x ∈ 1.

Apply SNoL_E 1 SNo_1 x Hx to the current goal.

Assume Hxa: SNo x.

rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).

Assume Hxb: SNoLev x ∈ 1.

Assume _.

We prove the intermediate claim L1: 0 = x.

Apply SNo_eq 0 x SNo_0 Hxa to the current goal.

We will prove SNoLev 0 = SNoLev x.

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

We will prove 0 = SNoLev x.

Apply cases_1 (SNoLev x) Hxb (λu ⇒ 0 = u) to the current goal.

We will prove 0 = 0.

Use reflexivity.

We will prove SNoEq_ (SNoLev 0) 0 x.

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

We will prove SNoEq_ 0 0 x.

Apply SNoEq_I to the current goal.

Let beta be given.

Assume Hb: beta ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE beta Hb.

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

An exact proof term for the current goal is In_0_1.

Let x be given.

Assume Hx: x ∈ 1.

We will prove x ∈ SNoL 1.

Apply cases_1 x Hx (λx ⇒ x ∈ SNoL 1) to the current goal.

We will prove 0 ∈ SNoL 1.

Apply SNoL_I 1 SNo_1 0 SNo_0 to the current goal.

We will prove SNoLev 0 ∈ SNoLev 1.

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

rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).

An exact proof term for the current goal is In_0_1.

We will prove 0 < 1.

An exact proof term for the current goal is ordinal_In_SNoLt 1 (nat_p_ordinal 1 nat_1) 0 In_0_1.