Let y be given.

Assume Hy1: SNo y.

Assume Hy2: SNoLev y ∈ SNoLev 0 ∩ SNoLev x.

We will prove False.

Apply EmptyE (SNoLev y) to the current goal.

We will prove SNoLev y ∈ 0.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from right to left).

We will prove SNoLev y ∈ SNoLev 0.

An exact proof term for the current goal is binintersectE1 (SNoLev 0) (SNoLev x) (SNoLev y) Hy2.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from left to right).

Assume H1: 0 ∈ SNoLev x.

Assume _.

Assume H2: 0 ∈ x.

We prove the intermediate claim L1: SNoLev x = 1.

Apply set_ext to the current goal.

An exact proof term for the current goal is Hxlow.

Let n be given.

Assume Hn: n ∈ 1.

Apply cases_1 n Hn to the current goal.

We will prove 0 ∈ SNoLev x.

An exact proof term for the current goal is H1.

Apply SNo_eq x 1 Hx SNo_1 to the current goal.

We will prove SNoLev x = SNoLev 1.

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

We will prove SNoLev x = 1.

An exact proof term for the current goal is L1.

We will prove SNoEq_ (SNoLev x) x 1.

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

We will prove SNoEq_ 1 x 1.

Let n be given.

Assume Hn: n ∈ 1.

We will prove n ∈ x ↔ n ∈ 1.

Apply cases_1 n Hn (λn ⇒ n ∈ x ↔ n ∈ 1) to the current goal.

We will prove 0 ∈ x ↔ 0 ∈ 1.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is In_0_1.

Assume _.

An exact proof term for the current goal is H2.

Assume H1: SNoLev x ∈ SNoLev 0.

We will prove False.

Apply EmptyE (SNoLev x) to the current goal.

We will prove SNoLev x ∈ 0.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from right to left).

We will prove SNoLev x ∈ SNoLev 0.

An exact proof term for the current goal is H1.