Let z be given.

Assume Hz: z ∈ X ∪ Y.

We will prove z ∈ ⋃ {X,Y}.

Apply (binunionE X Y z Hz) to the current goal.

Assume HzX: z ∈ X.

Apply (UnionI {X,Y} z X) to the current goal.

An exact proof term for the current goal is HzX.

An exact proof term for the current goal is (UPairI1 X Y).

Assume HzY: z ∈ Y.

Apply (UnionI {X,Y} z Y) to the current goal.

An exact proof term for the current goal is HzY.

An exact proof term for the current goal is (UPairI2 X Y).

Let z be given.

Assume Hz: z ∈ ⋃ {X,Y}.

We will prove z ∈ X ∪ Y.

Apply (UnionE_impred {X,Y} z Hz) to the current goal.

Let Z be given.

Assume HzZ: z ∈ Z.

Assume HZ: Z ∈ {X,Y}.

We prove the intermediate claim Hor: Z = X ∨ Z = Y.

An exact proof term for the current goal is (UPairE Z X Y HZ).

Apply Hor to the current goal.

Assume HZX: Z = X.

We prove the intermediate claim HzX: z ∈ X.

rewrite the current goal using HZX (from right to left).

An exact proof term for the current goal is HzZ.

An exact proof term for the current goal is (binunionI1 X Y z HzX).

Assume HZY: Z = Y.

We prove the intermediate claim HzY: z ∈ Y.

rewrite the current goal using HZY (from right to left).

An exact proof term for the current goal is HzZ.

An exact proof term for the current goal is (binunionI2 X Y z HzY).