An exact proof term for the current goal is (metric_topology_first_countable real_sequences uniform_metric_Romega uniform_metric_Romega_is_metric).