Let α be given.
Assume Ha: ordinal α.
We prove the intermediate claim La1: SNo α.
An exact proof term for the current goal is ordinal_SNo α Ha.
We prove the intermediate claim La2: SNoLev α = α.
An exact proof term for the current goal is ordinal_SNoLev α Ha.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ SNoL α.
Apply SNoL_E α La1 x Hx to the current goal.
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ SNoLev α.
Assume Hx3: x < α.
We will prove x ∈ SNoS_ α.
rewrite the current goal using La2 (from right to left).
We will prove x ∈ SNoS_ (SNoLev α).
Apply SNoS_I2 x α Hx1 La1 to the current goal.
We will prove SNoLev x ∈ SNoLev α.
An exact proof term for the current goal is Hx2.
Let x be given.
Assume Hx: x ∈ SNoS_ α.
Apply SNoS_E2 α Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ α.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove x ∈ SNoL α.
Apply SNoL_I α La1 x Hx3 to the current goal.
We will prove SNoLev x ∈ SNoLev α.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hx1.
We will prove x < α.
An exact proof term for the current goal is ordinal_SNoLev_max α Ha x Hx3 Hx1.
∎