Let y be given.

Assume Hy: y ∈ image_of f Empty.

Apply (ReplE_impred Empty (λx : set ⇒ apply_fun f x) y Hy) to the current goal.

Let x be given.

Assume HxE: x ∈ Empty.

Assume Hyx: y = apply_fun f x.

Apply FalseE to the current goal.

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

Let y be given.

Assume Hy: y ∈ Empty.

Apply FalseE to the current goal.

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