Let X and Y be given.

Assume HcountX: countable X.

We will prove countable (X ∩ Y).

Apply (Subq_countable (X ∩ Y) X HcountX) to the current goal.

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

∎