Let X, Tx, Y, Ty and f be given.
Assume Hhom: homeomorphism X Tx Y Ty f.
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume Heq: apply_fun f x1 = apply_fun f x2.
We will prove x1 = x2.
We prove the intermediate claim Hexg: ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).
An exact proof term for the current goal is (andER (continuous_map X Tx Y Ty f) (∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y)) Hhom).
Apply Hexg to the current goal.
Let g be given.
Assume Hgprop.
We prove the intermediate claim Hginv: ∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) (andEL (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgprop)).
rewrite the current goal using (Hginv x1 Hx1X) (from right to left).
rewrite the current goal using (Hginv x2 Hx2X) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
∎