We will prove ¬ (Sbar_Omega = setprod R R).

Assume Heq: Sbar_Omega = setprod R R.

Apply FalseE to the current goal.

We prove the intermediate claim Hord: ordinal (setprod R R).

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

An exact proof term for the current goal is Sbar_Omega_ordinal.

An exact proof term for the current goal is (not_ordinal_setprod_R_R Hord).

∎