Let α and β be given.
Assume Ha Hb.
Assume H1.
Apply ordinal_In_Or_Subq α β Ha Hb to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: β ⊆ α.
We will prove False.
Apply SNoLt_irref α to the current goal.
We will prove α < α.
Apply SNoLtLe_tra α β α (ordinal_SNo α Ha) (ordinal_SNo β Hb) (ordinal_SNo α Ha) H1 to the current goal.
We will prove β ≤ α.
An exact proof term for the current goal is ordinal_Subq_SNoLe β α Hb Ha H2.
∎