Let x be given.
Assume Hx Hxpos Hxlow.
Apply SNoLtE 0 x SNo_0 Hx Hxpos to the current goal.
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.
∎