Let x be given.

Assume Hx: x ∈ ⋃ Empty.

We will prove x ∈ Empty.

Apply (UnionE_impred Empty x Hx (x ∈ Empty)) to the current goal.

Let U be given.

Assume _: x ∈ U.

Assume HU: U ∈ Empty.

An exact proof term for the current goal is (EmptyE U HU (x ∈ Empty)).

Let x be given.

Assume Hx: x ∈ Empty.

We will prove x ∈ ⋃ Empty.

An exact proof term for the current goal is (EmptyE x Hx (x ∈ ⋃ Empty)).