Let X and Y be given.

Apply set_ext to the current goal.

An exact proof term for the current goal is (binintersect_com_Subq X Y).

An exact proof term for the current goal is (binintersect_com_Subq Y X).

∎