We will prove countable_set rational_numbers.
We will prove countable rational_numbers.
We prove the intermediate claim Hequip: equip ω rational_numbers.
We prove the intermediate claim HdefQ: rational_numbers = rational.
Use reflexivity.
rewrite the current goal using HdefQ (from left to right).
An exact proof term for the current goal is form100_3.
We prove the intermediate claim Hequip_sym: equip rational_numbers ω.
An exact proof term for the current goal is (equip_sym ω rational_numbers Hequip).
An exact proof term for the current goal is (equip_atleastp rational_numbers ω Hequip_sym).
∎