Assume Heq: setprod R R = setprod 2 ω.
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 Heps1SNoS: eps_ 1 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).
We prove the intermediate claim HepsR: eps_ 1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).
We prove the intermediate claim HpRR: (eps_ 1,0) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) 0 HepsR real_0).
We prove the intermediate claim Hp2o: (eps_ 1,0) ∈ setprod 2 ω.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HpRR.
We prove the intermediate claim Heps2: ((eps_ 1,0) 0) ∈ 2.
An exact proof term for the current goal is (ap0_Sigma 2 (λ_ : set ⇒ ω) (eps_ 1,0) Hp2o).
We prove the intermediate claim Heps2': eps_ 1 ∈ 2.
rewrite the current goal using (tuple_2_0_eq (eps_ 1) 0) (from right to left).
An exact proof term for the current goal is Heps2.
An exact proof term for the current goal is (eps_1_not_in_2 Heps2').
∎