Let alpha and beta be given.

Assume Ha Hb.

Apply Ha to the current goal.

Assume Ha1 _.

Apply Hb to the current goal.

Assume Hb1 _.

Apply ordinal_linear alpha beta Ha Hb to the current goal.

rewrite the current goal using Subq_binunion_eq (from left to right).

Assume H1: alpha ∪ beta = beta.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Hb.

rewrite the current goal using Subq_binunion_eq (from left to right).

rewrite the current goal using binunion_com (from left to right).

Assume H1: alpha ∪ beta = alpha.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Ha.

∎