Let X, Y and w be given.

Assume H1: w ∈ X ∪ Y.

We will prove w ∈ Y ∪ X.

Apply (binunionE X Y w H1) to the current goal.

Assume H2: w ∈ X.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H2.

Assume H2: w ∈ Y.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

∎