Let F be given.

Apply (Empty_eq {F x|x ∈ Empty}) to the current goal.

Let y be given.

Assume H1: y ∈ {F x|x ∈ Empty}.

Apply (ReplE_impred Empty F y H1) to the current goal.

Let x be given.

Assume H2: x ∈ Empty.

Assume _.

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

∎