Let X and Tx be given.
Assume Hmet.
We will prove normal_space X Tx.
Apply Hmet to the current goal.
Let d be given.
Assume HdPair.
We prove the intermediate claim Hd: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (metric_topology X d = Tx) HdPair).
We prove the intermediate claim Heq: metric_topology X d = Tx.
An exact proof term for the current goal is (andER (metric_on X d) (metric_topology X d = Tx) HdPair).
We prove the intermediate claim Hnorm: normal_space X (metric_topology X d).
An exact proof term for the current goal is (metrizable_spaces_normal X d Hd).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hnorm.
∎