Let X be given.

Assume H1.

Apply Empty_eq to the current goal.

Let x be given.

Assume Hx.

We will prove False.

Apply H1 to the current goal.

Let f be given.

Assume Hf: bij X 0 f.

Apply bijE X 0 f Hf to the current goal.

Assume Hf1: ∀x ∈ X, f x ∈ 0.

We will prove False.

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

∎