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_In_Or_Subq α β Ha Hb to the current goal.

Assume H1: α ∈ β.

rewrite the current goal using binintersect_Subq_eq_1 α β (Hb1 α H1) (from left to right).

An exact proof term for the current goal is Ha.

Assume H1: β ⊆ α.

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

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

An exact proof term for the current goal is Hb.

∎