Assume Hord: ordinal (setprod R R).

Apply FalseE to the current goal.

We prove the intermediate claim Hsing: {1} ∈ setprod R R.

An exact proof term for the current goal is Sing1_in_setprod_R_R.

We prove the intermediate claim HordSing: ordinal {1}.

An exact proof term for the current goal is (ordinal_Hered (setprod R R) Hord {1} Hsing).

An exact proof term for the current goal is (not_ordinal_Sing1 HordSing).

∎