Let α be given.

Assume Ha: ordinal α.

Let β be given.

Assume Hb: β ∈ α.

We prove the intermediate claim Lb: ordinal β.

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

We prove the intermediate claim Lb1: SNo β.

An exact proof term for the current goal is ordinal_SNo β Lb.

We prove the intermediate claim Lb2: SNoLev β = β.

An exact proof term for the current goal is ordinal_SNoLev β Lb.

Apply ordinal_SNoLev_max α Ha β Lb1 to the current goal.

We will prove SNoLev β ∈ α.

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

An exact proof term for the current goal is Hb.

∎