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 β be given.

Assume Hb: β ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE β 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.