Assume Heq: R = ω.

We will prove False.

We prove the intermediate claim HdefR: R = real.

Use reflexivity.

We prove the intermediate claim Heq': real = ω.

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 Homega_countable: atleastp ω ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

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 Homega_countable.

An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hreal_countable).

∎