Let X and f be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f Empty.
We will prove x ∈ Empty.
We prove the intermediate claim HfxE: apply_fun f x ∈ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ Empty) x Hx).
An exact proof term for the current goal is (FalseE ((EmptyE (apply_fun f x)) HfxE) (x ∈ Empty)).
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ preimage_of X f Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx).
∎