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