Let X, Y and Z be given.

Apply set_ext to the current goal.

Let w be given.

Assume H1: w ∈ X ∪ (Y ∪ Z).

We will prove w ∈ (X ∪ Y) ∪ Z.

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

Assume H2: w ∈ X.

Apply binunionI1 to the current goal.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

Assume H2: w ∈ Y ∪ Z.

Apply (binunionE Y Z w H2) to the current goal.

Assume H3: w ∈ Y.

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: w ∈ Z.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H3.

Let w be given.

Assume H1: w ∈ (X ∪ Y) ∪ Z.

We will prove w ∈ X ∪ (Y ∪ Z).

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

Assume H2: w ∈ X ∪ Y.

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

Assume H3: w ∈ X.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: w ∈ Y.

Apply binunionI2 to the current goal.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H3.

Assume H2: w ∈ Z.

Apply binunionI2 to the current goal.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is H2.

∎