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

Assume H1: alpha ∈ beta.

rewrite the current goal using binintersect_Subq_eq_1 alpha beta (Hb1 alpha H1) (from left to right).

An exact proof term for the current goal is Ha.

Assume H1: beta ⊆ alpha.

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

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

An exact proof term for the current goal is Hb.

∎