Let W, Y and A be given.
Assume Hsub: A ⊆ Y.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (W ∩ Y) ∩ A.
We prove the intermediate claim Hpair: x ∈ W ∩ Y ∧ x ∈ A.
An exact proof term for the current goal is (binintersectE (W ∩ Y) A x Hx).
We prove the intermediate claim HWY: x ∈ W ∩ Y.
An exact proof term for the current goal is (andEL (x ∈ W ∩ Y) (x ∈ A) Hpair).
We prove the intermediate claim HA: x ∈ A.
An exact proof term for the current goal is (andER (x ∈ W ∩ Y) (x ∈ A) Hpair).
We prove the intermediate claim HWYpair: x ∈ W ∧ x ∈ Y.
An exact proof term for the current goal is (binintersectE W Y x HWY).
We prove the intermediate claim HW: x ∈ W.
An exact proof term for the current goal is (andEL (x ∈ W) (x ∈ Y) HWYpair).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HW.
An exact proof term for the current goal is HA.
Let x be given.
Assume Hx: x ∈ W ∩ A.
We prove the intermediate claim Hpair: x ∈ W ∧ x ∈ A.
An exact proof term for the current goal is (binintersectE W A x Hx).
We prove the intermediate claim HW: x ∈ W.
An exact proof term for the current goal is (andEL (x ∈ W) (x ∈ A) Hpair).
We prove the intermediate claim HA: x ∈ A.
An exact proof term for the current goal is (andER (x ∈ W) (x ∈ A) Hpair).
We prove the intermediate claim HY: x ∈ Y.
An exact proof term for the current goal is (Hsub x HA).
We prove the intermediate claim HWY: x ∈ W ∩ Y.
An exact proof term for the current goal is (binintersectI W Y x HW HY).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HWY.
An exact proof term for the current goal is HA.
∎