Let alpha be given.
Assume Ha: ordinal alpha.
Apply Ha to the current goal.
Assume Ha1 _.
Let z be given.
Assume Hz: SNo z.
Assume Hz2: SNoLev z ∈ ordsucc 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 ordsuccE alpha (SNoLev z) Hz2 to the current goal.
Assume Hz3: SNoLev z ∈ alpha.
We will prove z ≤ alpha.
Apply SNoLtLe to the current goal.
We will prove z < alpha.
An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha z Hz Hz3.
Assume Hz3: SNoLev z = alpha.
Apply dneg to the current goal.
Assume H1: ¬ (z ≤ alpha).
We prove the intermediate claim L1: ∀beta, ordinal beta → beta ∈ alpha → beta ∈ z.
Apply ordinal_ind to the current goal.
Let beta be given.
Assume Hb: ordinal beta.
Assume IH: ∀gamma ∈ beta, gamma ∈ alpha → gamma ∈ z.
Assume Hb2: beta ∈ alpha.
Apply dneg to the current goal.
Assume H2: beta ∉ z.
Apply H1 to the current goal.
Apply SNoLtLe to the current goal.
We will prove z < alpha.
We prove the intermediate claim Lb1: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
We prove the intermediate claim Lb2: SNoLev beta = beta.
An exact proof term for the current goal is ordinal_SNoLev beta Hb.
Apply SNoLt_tra z beta alpha Hz Lb1 La1 to the current goal.
We will prove z < beta.
Apply SNoLtI3 to the current goal.
We will prove SNoLev beta ∈ SNoLev z.
rewrite the current goal using Lb2 (from left to right).
rewrite the current goal using Hz3 (from left to right).
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove SNoEq_ (SNoLev beta) z beta.
rewrite the current goal using Lb2 (from left to right).
Let gamma be given.
Assume Hc: gamma ∈ beta.
We will prove gamma ∈ z ↔ gamma ∈ beta.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is Hc.
Assume _.
We will prove gamma ∈ z.
Apply IH gamma Hc to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb2 gamma Hc.
We will prove SNoLev beta ∉ z.
rewrite the current goal using Lb2 (from left to right).
We will prove beta ∉ z.
An exact proof term for the current goal is H2.
We will prove beta < alpha.
An exact proof term for the current goal is ordinal_In_SNoLt alpha Ha beta Hb2.
We prove the intermediate claim L2: alpha ⊆ z.
Let beta be given.
Assume Hb: beta ∈ alpha.
An exact proof term for the current goal is L1 beta (ordinal_Hered alpha Ha beta Hb) Hb.
We prove the intermediate claim L3: z = alpha.
Apply SNo_eq z alpha Hz La1 to the current goal.
We will prove SNoLev z = SNoLev alpha.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hz3.
We will prove SNoEq_ (SNoLev z) z alpha.
rewrite the current goal using Hz3 (from left to right).
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove beta ∈ z ↔ beta ∈ alpha.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is Hb.
Assume _.
An exact proof term for the current goal is L2 beta Hb.
Apply H1 to the current goal.
We will prove z ≤ alpha.
rewrite the current goal using L3 (from left to right).
We will prove alpha ≤ alpha.
Apply SNoLe_ref to the current goal.
∎