Let U1, V1, U2 and V2 be given.
We will prove setprod U1 V1 ∩ setprod U2 V2 = setprod (U1 ∩ U2) (V1 ∩ V2).
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ setprod U1 V1 ∩ setprod U2 V2.
We will prove p ∈ setprod (U1 ∩ U2) (V1 ∩ V2).
We prove the intermediate claim HpU1V1: p ∈ setprod U1 V1.
An exact proof term for the current goal is (binintersectE1 (setprod U1 V1) (setprod U2 V2) p Hp).
We prove the intermediate claim HpU2V2: p ∈ setprod U2 V2.
An exact proof term for the current goal is (binintersectE2 (setprod U1 V1) (setprod U2 V2) p Hp).
We prove the intermediate claim Hp0U1: p 0 ∈ U1.
An exact proof term for the current goal is (ap0_Sigma U1 (λu ⇒ V1) p HpU1V1).
We prove the intermediate claim Hp1V1: p 1 ∈ V1.
An exact proof term for the current goal is (ap1_Sigma U1 (λu ⇒ V1) p HpU1V1).
We prove the intermediate claim Hp0U2: p 0 ∈ U2.
An exact proof term for the current goal is (ap0_Sigma U2 (λu ⇒ V2) p HpU2V2).
We prove the intermediate claim Hp1V2: p 1 ∈ V2.
An exact proof term for the current goal is (ap1_Sigma U2 (λu ⇒ V2) p HpU2V2).
We prove the intermediate claim Hp0: p 0 ∈ U1 ∩ U2.
An exact proof term for the current goal is (binintersectI U1 U2 (p 0) Hp0U1 Hp0U2).
We prove the intermediate claim Hp1: p 1 ∈ V1 ∩ V2.
An exact proof term for the current goal is (binintersectI V1 V2 (p 1) Hp1V1 Hp1V2).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U1 V1 p HpU1V1).
rewrite the current goal using Heta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (U1 ∩ U2) (V1 ∩ V2) (p 0) (p 1) Hp0 Hp1).
Let p be given.
Assume Hp: p ∈ setprod (U1 ∩ U2) (V1 ∩ V2).
We will prove p ∈ setprod U1 V1 ∩ setprod U2 V2.
We prove the intermediate claim Hp0: p 0 ∈ U1 ∩ U2.
An exact proof term for the current goal is (ap0_Sigma (U1 ∩ U2) (λu ⇒ V1 ∩ V2) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ V1 ∩ V2.
An exact proof term for the current goal is (ap1_Sigma (U1 ∩ U2) (λu ⇒ V1 ∩ V2) p Hp).
We prove the intermediate claim Hp0U1: p 0 ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 U2 (p 0) Hp0).
We prove the intermediate claim Hp0U2: p 0 ∈ U2.
An exact proof term for the current goal is (binintersectE2 U1 U2 (p 0) Hp0).
We prove the intermediate claim Hp1V1: p 1 ∈ V1.
An exact proof term for the current goal is (binintersectE1 V1 V2 (p 1) Hp1).
We prove the intermediate claim Hp1V2: p 1 ∈ V2.
An exact proof term for the current goal is (binintersectE2 V1 V2 (p 1) Hp1).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta (U1 ∩ U2) (V1 ∩ V2) p Hp).
rewrite the current goal using Heta (from left to right).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U1 V1 (p 0) (p 1) Hp0U1 Hp1V1).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U2 V2 (p 0) (p 1) Hp0U2 Hp1V2).
∎