Let X, Tx, Y, U, V, VU and VV be given.
Assume HU: U = VU ∩ Y.
Assume HV: V = VV ∩ Y.
We will prove U ∩ V = (VU ∩ VV) ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∩ V.
We prove the intermediate claim HxUV: x ∈ U ∧ x ∈ V.
An exact proof term for the current goal is (binintersectE U V x Hx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (x ∈ V) HxUV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andER (x ∈ U) (x ∈ V) HxUV).
We prove the intermediate claim HxUY: x ∈ VU ∩ Y.
rewrite the current goal using HU (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HxVY: x ∈ VV ∩ Y.
rewrite the current goal using HV (from right to left).
An exact proof term for the current goal is HxV.
We prove the intermediate claim HxVU: x ∈ VU.
An exact proof term for the current goal is (binintersectE1 VU Y x HxUY).
We prove the intermediate claim HxVV: x ∈ VV.
An exact proof term for the current goal is (binintersectE1 VV Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 VU Y x HxUY).
We prove the intermediate claim HxVUVV: x ∈ VU ∩ VV.
An exact proof term for the current goal is (binintersectI VU VV x HxVU HxVV).
An exact proof term for the current goal is (binintersectI (VU ∩ VV) Y x HxVUVV HxY).
Let x be given.
Assume Hx: x ∈ (VU ∩ VV) ∩ Y.
We prove the intermediate claim HxVUVV: x ∈ VU ∩ VV.
An exact proof term for the current goal is (binintersectE1 (VU ∩ VV) Y x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 (VU ∩ VV) Y x Hx).
We prove the intermediate claim HxVU: x ∈ VU.
An exact proof term for the current goal is (binintersectE1 VU VV x HxVUVV).
We prove the intermediate claim HxVV: x ∈ VV.
An exact proof term for the current goal is (binintersectE2 VU VV x HxVUVV).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HU (from left to right).
An exact proof term for the current goal is (binintersectI VU Y x HxVU HxY).
We prove the intermediate claim HxV: x ∈ V.
rewrite the current goal using HV (from left to right).
An exact proof term for the current goal is (binintersectI VV Y x HxVV HxY).
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
∎