Let X, Tx, Y, d1 and d2 be given.
Assume HTx: topology_on X Tx.
Assume Hd1: metric_on Y d1.
Assume Hd2: metric_on Y d2.
Assume Htop: metric_topology Y d1 = metric_topology Y d2.
rewrite the current goal using (compact_open_eq_compact_convergence_on_C X Tx Y d1 HTx Hd1) (from right to left).
rewrite the current goal using (compact_open_eq_compact_convergence_on_C X Tx Y d2 HTx Hd2) (from right to left).
rewrite the current goal using Htop (from left to right).
Use reflexivity.
∎