Assume Heq: setprod R R = R.

We will prove False.

We prove the intermediate claim HpRR: (0,1) ∈ setprod R R.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 0 1 real_0 real_1).

We prove the intermediate claim HpR: (0,1) ∈ R.

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

An exact proof term for the current goal is HpRR.

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

rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left) at position 1.

An exact proof term for the current goal is HpR.

We prove the intermediate claim HdefR: R = real.

Use reflexivity.

We prove the intermediate claim HSing1real: {1} ∈ real.

rewrite the current goal using HdefR (from right to left) at position 1.

An exact proof term for the current goal is HSing1R.

We prove the intermediate claim HSNo: SNo {1}.

An exact proof term for the current goal is (real_SNo {1} HSing1real).

An exact proof term for the current goal is (Sing1_not_SNo HSNo).

∎