Assume Heq: ordered_square = setprod R R.

We will prove False.

Set p to be the term (2,2).

We prove the intermediate claim HpRR: p ∈ setprod R R.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 2 2 two_in_R two_in_R).

We prove the intermediate claim HpOS: p ∈ ordered_square.

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

An exact proof term for the current goal is HpRR.

We prove the intermediate claim HpSing: p ∈ setprod {2} {2}.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {2} {2} 2 2 (SingI 2) (SingI 2)).

We prove the intermediate claim Hcoords: 2 ∈ unit_interval ∧ 2 ∈ unit_interval.

An exact proof term for the current goal is (setprod_coords_in 2 2 unit_interval unit_interval p HpSing HpOS).

We prove the intermediate claim H2I: 2 ∈ unit_interval.

An exact proof term for the current goal is (andEL (2 ∈ unit_interval) (2 ∈ unit_interval) Hcoords).

An exact proof term for the current goal is (two_not_in_unit_interval H2I).

∎