Let V and y be given.

Assume Hy: y ∈ V.

We will prove V ≠ Empty.

Assume HV: V = Empty.

We prove the intermediate claim HyE: y ∈ Empty.

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

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is (EmptyE y HyE).

∎