Assume Heq: setprod 2 ω = setprod R R.

We will prove False.

Apply setprod_R_R_neq_setprod_2_omega to the current goal.

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

Use reflexivity.

∎