Suppose $X$ is a length metric space and $G$ acts on $X$ by isometries properly discontinuously and the action is free. Then there is unique length metric on $X/G$ such that $\pi : X \rightarrow X/G$ is a local isometry.
My attempt: Let $x, y \in X$, $\pi(x) = \bar{x}, \pi (y) =\bar{y}$.
Now I define $$\bar{d}(x,y) = d(\pi^{-1} (\bar{x}), \pi^{-1} (\bar{y})) = \text{inf}\{d(x^\prime, y^\prime) \mid x^\prime \in \pi^{-1} (\bar{x}), y^\prime \in \pi^{-1} (\bar{y})\}$$
my thought is to claim $\bar{d}$ is the required metric. But I cannot approach properly. Please help.