Let α and β be given.

Assume Ha Hb.

Apply Ha to the current goal.

Assume Ha1 _.

Apply Hb to the current goal.

Assume Hb1 _.

Apply ordinal_linear α β Ha Hb to the current goal.

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

Assume H1: α ∪ β = β.

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: α ∪ β = α.

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

An exact proof term for the current goal is Ha.

∎