Let X and Y be given.

Assume Heq: equip X Y.

Assume HcountY: countable_set Y.

An exact proof term for the current goal is (equip_countable_set_left Y X (equip_sym X Y Heq) HcountY).

∎