Let alpha be given.
Assume Ha: ordinal 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.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ SNoL alpha.
Apply SNoL_E alpha La1 x Hx to the current goal.
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ SNoLev alpha.
Assume Hx3: x < alpha.
We will prove x ∈ SNoS_ alpha.
rewrite the current goal using La2 (from right to left).
We will prove x ∈ SNoS_ (SNoLev alpha).
Apply SNoS_I2 x alpha Hx1 La1 to the current goal.
We will prove SNoLev x ∈ SNoLev alpha.
An exact proof term for the current goal is Hx2.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove x ∈ SNoL alpha.
Apply SNoL_I alpha La1 x Hx3 to the current goal.
We will prove SNoLev x ∈ SNoLev alpha.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hx1.
We will prove x < alpha.
An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha x Hx3 Hx1.
∎