We will prove ¬ (Sbar_Omega = setprod 2 ω).
Assume Heq: Sbar_Omega = setprod 2 ω.
Apply FalseE to the current goal.
We prove the intermediate claim H2count: countable 2.
An exact proof term for the current goal is (finite_countable 2 (nat_finite 2 nat_2)).
We prove the intermediate claim HomegaCount: countable ω.
An exact proof term for the current goal is omega_countable_set.
We prove the intermediate claim HprodCount: countable (setprod 2 ω).
An exact proof term for the current goal is (setprod_countable 2 ω H2count HomegaCount).
We prove the intermediate claim HcountSbar: countable_set Sbar_Omega.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HprodCount.
An exact proof term for the current goal is (Sbar_Omega_uncountable HcountSbar).
∎