Let X, Y and z be given.

Assume H1: z ∈ X.

We will prove z ∈ X ∪ Y.

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

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

We will prove z ∈ X.

An exact proof term for the current goal is H1.

We will prove X ∈ {X,Y}.

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

∎