Let X, Y, U and V be given.
Assume HU: U ⊆ X.
Assume HV: V ⊆ Y.
We will prove rectangle_set U V = (rectangle_set U Y) ∩ (rectangle_set X V).
We will prove setprod U V = (setprod U Y) ∩ (setprod X V).
We prove the intermediate claim Hinter: setprod U Y ∩ setprod X V = setprod (U ∩ X) (Y ∩ V).
An exact proof term for the current goal is (setprod_intersection U Y X V).
rewrite the current goal using Hinter (from left to right).
We prove the intermediate claim HUcap: U ∩ X = U.
An exact proof term for the current goal is (binintersect_Subq_eq_1 U X HU).
We prove the intermediate claim HYcap: Y ∩ V = V.
rewrite the current goal using (binintersect_com Y V) (from left to right).
An exact proof term for the current goal is (binintersect_Subq_eq_1 V Y HV).
rewrite the current goal using HUcap (from left to right).
rewrite the current goal using HYcap (from left to right).
Use reflexivity.
∎