Let A be given.

Apply Empty_Subq_eq to the current goal.

An exact proof term for the current goal is (binintersect_Subq_1 Empty A).

∎