Let α be given.
Assume Ha.
Apply ordinal_In_Or_Subq 0 (ordsucc α) ordinal_Empty (ordinal_ordsucc α Ha) to the current goal.
Assume H1: 0 ∈ ordsucc α.
An exact proof term for the current goal is H1.
Assume H1: ordsucc α ⊆ 0.
We will prove False.
Apply EmptyE α to the current goal.
We will prove α ∈ 0.
Apply H1 to the current goal.
Apply ordsuccI2 to the current goal.
∎