We prove the intermediate claim Hunc: atleastp ω real ∧ ¬ equip real ω.

An exact proof term for the current goal is form100_22_real_uncountable.

We prove the intermediate claim Hatleast: atleastp ω real.

An exact proof term for the current goal is (andEL (atleastp ω real) (¬ equip real ω) Hunc).

We will prove infinite R.

An exact proof term for the current goal is (atleastp_omega_infinite real Hatleast).

∎