Let x be given.

Assume Hx: x ∈ U ∪ V.

Apply (binunionE U V x Hx) to the current goal.

Assume HxU: x ∈ U.

Apply (UnionI (UPair U V) x U HxU) to the current goal.

An exact proof term for the current goal is (UPairI1 U V).

Assume HxV: x ∈ V.

Apply (UnionI (UPair U V) x V HxV) to the current goal.

An exact proof term for the current goal is (UPairI2 U V).

Let x be given.

Assume Hx: x ∈ ⋃ (UPair U V).

Apply (UnionE_impred (UPair U V) x Hx (x ∈ U ∪ V)) to the current goal.

Let Z be given.

Assume HxZ: x ∈ Z.

Assume HZin: Z ∈ UPair U V.

Apply (UPairE Z U V HZin) to the current goal.

Assume HZeqU: Z = U.

We prove the intermediate claim HxU: x ∈ U.

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

An exact proof term for the current goal is HxZ.

An exact proof term for the current goal is (binunionI1 U V x HxU).

Assume HZeqV: Z = V.

We prove the intermediate claim HxV: x ∈ V.

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

An exact proof term for the current goal is HxZ.

An exact proof term for the current goal is (binunionI2 U V x HxV).