Let alpha be given.

Assume Ha.

Let beta be given.

Assume Hb.

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

An exact proof term for the current goal is ordinal_ordsucc_In_Subq alpha Ha beta Hb.

Apply ordinal_In_Or_Subq (ordsucc beta) alpha (ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb)) Ha to the current goal.

Assume H1: ordsucc beta ∈ alpha.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: alpha ⊆ ordsucc beta.

We prove the intermediate claim L2: ordsucc beta = alpha.

Apply set_ext to the current goal.

An exact proof term for the current goal is L1.

An exact proof term for the current goal is H1.

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

Apply ordsuccI2 to the current goal.

∎