We will prove {1} ∈ setprod R R.

We prove the intermediate claim HRdef: R = real.

Use reflexivity.

We prove the intermediate claim H0R: 0 ∈ R.

An exact proof term for the current goal is (mem_eqL 0 R real HRdef real_0).

We prove the intermediate claim H1R: 1 ∈ R.

An exact proof term for the current goal is (mem_eqL 1 R real HRdef real_1).

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

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

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

An exact proof term for the current goal is Hpair.

∎