Let X, d, seq and x be given.

Assume H: sequence_converges_metric X d seq x.

We will prove sequence_converges_metric X d seq x.

An exact proof term for the current goal is H.

∎