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