Howto formally go about proving that two LTL formulas are equivalent?
The semantics of LTL is (initially) defined with respect to infinite computations. So in that sense, two formulas $\psi_1,\psi_2$ are equivalent if for every computation $\pi$ it holds that $\pi\models \psi_1$ iff $\pi\models \psi_2$.

So in this sense - yes, you need the formulas to unwind the same set of computations.

The semantics is then extended to Kripke structures in the $ALTL$ model, meaning that a formula is satisfied in a structure if all its computations satisfy the formula. However, testing for equivalence should be done with respect to paths.

As for proving formally the equivalence of formulas: if this is an exercise, it will probably be easiest to analyze the formulas and prove that a path satisfies the first iff it satisfies the second. However, if you are handling complex formulas, then the best approach will probably be via nondeterministic Buchi automata, by testing the equivalence of the automata that correspond to the formulas. In practice, there are tools to do just that, but doing it manually may prove quite time-consuming (as the problem is PSPACE complete).