Assume Heq: setprod 2 ω = rational_numbers.
We will prove False.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hp: (0,1) ∈ setprod 2 ω.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 1 In_0_2 H1omega).
We prove the intermediate claim HpQ: (0,1) ∈ rational_numbers.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim HSingQ: {1} ∈ rational_numbers.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpQ.
We prove the intermediate claim HSingR: {1} ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R {1} HSingQ).
We prove the intermediate claim HSingS: SNo {1}.
An exact proof term for the current goal is (real_SNo {1} HSingR).
An exact proof term for the current goal is (Sing1_not_SNo HSingS).
∎