We will prove TransSet Empty ∧ ∀x ∈ Empty, TransSet x.

Apply andI to the current goal.

Let x be given.

Assume Hx: x ∈ Empty.

We will prove False.

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

Let x be given.

Assume Hx: x ∈ Empty.

We will prove False.

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

∎