Let X, Y, f and y be given.
Assume Hbij: bijection X Y f.
Assume Hy: y ∈ Y.
Apply Hbij to the current goal.
Assume Hfun: function_on f X Y.
Assume Huniq.
Apply (Huniq y Hy) to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ apply_fun f x = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x).
We use x to witness the existential quantifier.
We prove the intermediate claim Hx0: x ∈ X ∧ apply_fun f x = y.
An exact proof term for the current goal is (andEL (x ∈ X ∧ apply_fun f x = y) (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x) Hx).
An exact proof term for the current goal is Hx0.
∎