Let X and Y be given.

Assume Heq: equip X Y.

Assume HcountX: countable_set X.

We will prove countable_set Y.

We prove the intermediate claim Heq_sym: equip Y X.

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

We prove the intermediate claim Hayx: atleastp Y X.

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

An exact proof term for the current goal is (atleastp_tra Y X ω Hayx HcountX).

∎