Let X and Y be given.
Assume H1: X ⊆ Y.
Apply set_ext to the current goal.
Apply binintersect_Subq_1 to the current goal.
Let x be given.
Assume H2: x ∈ X.
Apply binintersectI to the current goal.
An exact proof term for the current goal is H2.
Apply H1 to the current goal.
An exact proof term for the current goal is H2.
∎