Let alpha be given.

Assume Ha.

Apply ordinal_In_SNoLt (ordsucc alpha) (ordinal_ordsucc alpha Ha) 0 to the current goal.

We will prove 0 ∈ ordsucc alpha.

An exact proof term for the current goal is ordinal_0_In_ordsucc alpha Ha.

∎