The answer is yesser than I thought. I mentioned this issue at http://eventos.cmm.uchile.cl/edynamicsxiii/, since the proximality lemma from my previous answer was discussed there. Someone pointed out that Hindman's original proof of his famous theorem is at least somewhat elementary in some technical sense, and implies a significant part of the proximality theorem, so the answer must be "yes" at least in some technical sense.
After a bit of searching I found the relevant paper [1]: in the sense of reverse mathematics, your theorem is provable in $\mathrm{ACA}_0^+$, which is some (not so strong) segment of second-order arithmetic. Disclaimer: I don't really know what this means.
I quote the relevant theorem in the form stated in this paper. They call this the Auslander-Ellis theorem (wasn't this Furstenberg's theorem? did he just observe the connection?)
Theorem. Let $X$ be a compact metric space and let $T : X \to X$ be continuous. Regard $(X,T)$ as dynamical system. Given $x \in X$, there exists $y \in X$ such that $y$ is uniformly recurrent and proximal to $x$.
They show that this theorem is provable in $\mathrm{ACA}_0^+$. Let me recall how to conclude your result (this deduction seems very elementary, so I guess it needs much less than $\mathrm{ACA}_0^+$).
Corollary. Every distal system is invertible.
Proof. Injectivity is clear. Take $x \in X$, and apply the previous theorem, to get that $x$ is proximal to some uniformly recurrent $y$. Then $x = y$, so every point in $X$ is uniformly recurrent. Clearly this implies surjectivity, since if $U$ is a neighborhood of any $x \in X$, we have $T^n(x) \in U$ for some positive $n$, and then $T^{n-1}(x)$ maps to $U$ in $T$, so $TX$ is dense in $X$ and by compactness is equal to $X$. Square.
Still, as mentioned in the first sentence of [1], "It is well known that all existing proofs of HT are nonconstructive.", and $\mathrm{ACA}_0^+$ is about quantifying this nonconstructivity. It is of course still entirely possible that the OP's theorem needs strictly less than the above theorem, and has some simple proof. I am not able to find a reduction of the proximality theorem or Hindman's theorem to the OP's problem.
Reference
[1]: Blass, Andreas R.; Hirst, Jeffry L.; Simpson, Stephen G., Logical analysis of some theorems of combinatorics and topological dynamics, Logic and combinatorics, Proc. AMS-IMS-SIAM Conf., Arcata/Calif. 1985, Contemp. Math. 65, 125-156 (1987). ZBL0652.03040.