Let X and Y be given.
Apply prop_ext_2 to the current goal.
Assume H1: X ⊆ Y.
We will prove X ∪ Y = Y.
Apply set_ext to the current goal.
We will prove X ∪ Y ⊆ Y.
Apply (binunion_Subq_min X Y Y) to the current goal.
We will prove X ⊆ Y.
An exact proof term for the current goal is H1.
We will prove Y ⊆ Y.
An exact proof term for the current goal is (Subq_ref Y).
We will prove Y ⊆ X ∪ Y.
An exact proof term for the current goal is (binunion_Subq_2 X Y).
Assume H1: X ∪ Y = Y.
We will prove X ⊆ Y.
rewrite the current goal using H1 (from right to left).
We will prove X ⊆ X ∪ Y.
An exact proof term for the current goal is (binunion_Subq_1 X Y).
∎