Let X, Y, f, u and v be given.
Assume Hbij: bijection X Y f.
Assume HuX: u ∈ X.
Assume HvX: v ∈ X.
Assume Heq: apply_fun f u = apply_fun f v.
Apply Hbij to the current goal.
Assume Hfun: function_on f X Y.
Assume Huniq.
We prove the intermediate claim HyY: apply_fun f u ∈ Y.
An exact proof term for the current goal is (Hfun u HuX).
Apply (Huniq (apply_fun f u) HyY) to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ apply_fun f x = apply_fun f u ∧ (∀x' : set, x' ∈ X → apply_fun f x' = apply_fun f u → x' = x).
We prove the intermediate claim Hxuniq: ∀x' : set, x' ∈ X → apply_fun f x' = apply_fun f u → x' = x.
An exact proof term for the current goal is (andER (x ∈ X ∧ apply_fun f x = apply_fun f u) (∀x' : set, x' ∈ X → apply_fun f x' = apply_fun f u → x' = x) Hx).
We prove the intermediate claim Hu: u = x.
Apply (Hxuniq u HuX) to the current goal.
Use reflexivity.
We prove the intermediate claim Hv: v = x.
Apply (Hxuniq v HvX) to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
rewrite the current goal using Hu (from left to right).
rewrite the current goal using Hv (from left to right).
Use reflexivity.
∎