Let α be given.

Assume Ha.

Let β be given.

Assume Hb.

We prove the intermediate claim L1: ordsucc β ⊆ α.

An exact proof term for the current goal is ordinal_ordsucc_In_Subq α Ha β Hb.

Apply ordinal_In_Or_Subq (ordsucc β) α (ordinal_ordsucc β (ordinal_Hered α Ha β Hb)) Ha to the current goal.

Assume H1: ordsucc β ∈ α.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: α ⊆ ordsucc β.

We prove the intermediate claim L2: ordsucc β = α.

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.

∎