Assume Heq: setprod 2 ω = R.
We will prove False.
We prove the intermediate claim Homega_countable: countable ω.
We will prove atleastp ω ω.
We prove the intermediate claim Homega_sub: ω ⊆ ω.
Let x be given.
Assume Hx: x ∈ ω.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (Subq_atleastp ω ω Homega_sub).
We prove the intermediate claim H01subomega: {0,1} ⊆ ω.
Let x be given.
Assume Hx: x ∈ {0,1}.
We will prove x ∈ ω.
Apply (UPairE x 0 1 Hx (x ∈ ω)) to the current goal.
Assume Hx0: x = 0.
rewrite the current goal using Hx0 (from left to right).
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Assume Hx1: x = 1.
rewrite the current goal using Hx1 (from left to right).
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H2subomega: 2 ⊆ ω.
An exact proof term for the current goal is (Subq_tra 2 {0,1} ω Subq_2_UPair01 H01subomega).
We prove the intermediate claim H2countable: countable 2.
An exact proof term for the current goal is (Subq_atleastp 2 ω H2subomega).
We prove the intermediate claim Hprod_countable: countable (setprod 2 ω).
An exact proof term for the current goal is (setprod_countable 2 ω H2countable Homega_countable).
We prove the intermediate claim HRcountable: countable R.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hprod_countable.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Hreal_countable: atleastp real ω.
rewrite the current goal using HdefR (from right to left) at position 1.
An exact proof term for the current goal is HRcountable.
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hreal_countable).
∎