Let alpha and beta be given.

Assume Ha Hb Hab.

We prove the intermediate claim L1: alpha ∈ ordsucc beta.

Apply ordinal_In_Or_Subq alpha beta Ha Hb to the current goal.

Assume H1: alpha ∈ beta.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: beta ⊆ alpha.

We prove the intermediate claim L1a: alpha = beta.

Apply set_ext to the current goal.

An exact proof term for the current goal is Hab.

An exact proof term for the current goal is H1.

rewrite the current goal using L1a (from left to right).

Apply ordsuccI2 to the current goal.

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 ordinal_SNoLev_max_2 beta Hb alpha La1 to the current goal.

We will prove SNoLev alpha ∈ ordsucc beta.

rewrite the current goal using La2 (from left to right).

An exact proof term for the current goal is L1.

∎