Assume Heq: R = rational_numbers.
We will prove False.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Heq': real = rational_numbers.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Heq.
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).
We prove the intermediate claim Hcount_Q: atleastp rational_numbers ω.
An exact proof term for the current goal is (equip_atleastp rational_numbers ω Hequip_sym).
We prove the intermediate claim Hreal_countable: atleastp real ω.
rewrite the current goal using Heq' (from left to right) at position 1.
An exact proof term for the current goal is Hcount_Q.
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hreal_countable).
∎