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