Let alpha be given.
Assume Ha: ordinal alpha.
Let z be given.
Assume Hz: SNo z.
Assume Hz2: SNoLev z ∈ alpha.
We prove the intermediate claim La1: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim La2: SNoLev alpha = alpha.
An exact proof term for the current goal is ordinal_SNoLev alpha Ha.
We will prove z < alpha.
Apply SNoLt_trichotomy_or z alpha Hz (ordinal_SNo alpha Ha) to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: z < alpha.
An exact proof term for the current goal is H1.
Assume H1: z = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using La2 (from right to left) at position 1.
We will prove SNoLev alpha ∈ alpha.
rewrite the current goal using H1 (from right to left) at position 1.
We will prove SNoLev z ∈ alpha.
An exact proof term for the current goal is Hz2.
Assume H1: alpha < z.
We will prove False.
Apply SNoLtE alpha z La1 Hz H1 to the current goal.
Let w be given.
rewrite the current goal using La2 (from left to right).
Assume Hw: SNo w.
Assume H2: SNoLev w ∈ alpha ∩ SNoLev z.
Assume H3: SNoEq_ (SNoLev w) w alpha.
Assume H4: SNoEq_ (SNoLev w) w z.
Assume H5: alpha < w.
Assume H6: w < z.
Assume H7: SNoLev w ∉ alpha.
We will prove False.
Apply H7 to the current goal.
An exact proof term for the current goal is binintersectE1 alpha (SNoLev z) (SNoLev w) H2.
rewrite the current goal using La2 (from left to right).
Assume H2: alpha ∈ SNoLev z.
We will prove False.
An exact proof term for the current goal is In_no2cycle alpha (SNoLev z) H2 Hz2.
rewrite the current goal using La2 (from left to right).
Assume H2: SNoLev z ∈ alpha.
Assume H3: SNoEq_ (SNoLev z) alpha z.
Assume H4: SNoLev z ∉ alpha.
An exact proof term for the current goal is H4 H2.
∎