Assume Hno: ¬ (∃y : set, y ∈ V).

We prove the intermediate claim HVsub: V ⊆ Empty.

Let y be given.

Assume Hy: y ∈ V.

We will prove y ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim Hexy: ∃z : set, z ∈ V.

We use y to witness the existential quantifier.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is (Hno Hexy).

We prove the intermediate claim HVEmpty: V = Empty.

An exact proof term for the current goal is (Empty_Subq_eq V HVsub).

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hne HVEmpty).