We will prove ¬ (Sbar_Omega = rational_numbers).

Assume Heq: Sbar_Omega = rational_numbers.

Apply FalseE to the current goal.

We prove the intermediate claim Hunc: uncountable_set rational_numbers.

rewrite the current goal using Heq (from right to left).

An exact proof term for the current goal is Sbar_Omega_uncountable.

An exact proof term for the current goal is (Hunc rational_numbers_countable).

∎