Let X and d be given.

Assume Hd: metric_on X d.

An exact proof term for the current goal is (completely_regular_space_implies_regular X (metric_topology X d) (metric_spaces_completely_regular X d Hd)).

∎