Let alpha be given.

Assume Ha: ordinal alpha.

Let beta be given.

Assume Hb: beta ∈ alpha.

We prove the intermediate claim Lb: ordinal beta.

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

We prove the intermediate claim Lb1: SNo beta.

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

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

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

Apply ordinal_SNoLev_max alpha Ha beta Lb1 to the current goal.

We will prove SNoLev beta ∈ alpha.

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

An exact proof term for the current goal is Hb.

∎