We will prove ¬ (Sbar_Omega = R).

Assume Heq: Sbar_Omega = R.

Apply FalseE to the current goal.

We prove the intermediate claim HSmem: S_Omega ∈ R.

An exact proof term for the current goal is (mem_eqR S_Omega Sbar_Omega R Heq S_Omega_in_Sbar_Omega).

An exact proof term for the current goal is (S_Omega_notin_R HSmem).

∎