@MatheinBoulomenos induction on the complexity of the formula
so divide your formula into cases
(next time ping me if I forget to reply :P)
for the first case: let the formula be $(f \land g)$. Then, $(f \land g$ is not a formula. It might be harder to argue that you can't cut off things from the right of $g$ to make $(f \land g$ a formula...
@MatheinBoulomenos I strongly recommend preferring your kind of approach rather than the author's, simply because it is more general and less ad-hoc. But an even better approach is to first prove unique parsing, namely that for every (propositional) formula x there is a unique main boolean operation and unique subformulae. More precisely, exactly one of the following cases holds:
(1) x = "¬"+y for unique formula y. (2) x = "("+y+"∧"+z+")" for unique formulae y,z. (3) x = "("+y+"∨"+z+")" for unique formulae y,z. (4) x = "("+y+"⇒"+z+")" for unique formulae y,z. (5) x = "("+y+"⇔"+z+")" for unique formulae y,z.
This is easy to prove by structural induction. Note that the definition of well-formed formula directly implies that at least one of these cases holds, but unique parsing says that exactly one of these cases holds.
Okay; it's easy after you prove that if the first symbol is not "¬" then the net open minus close brackets is positive until the end (where it is zero). (Is this your parenthesis counting lemma?) Now to prove unique parsing, say (2) and (3) both hold, then you must have formulae y0,y1 such that y0 is a strict prefix of y1. Either both y0,y1 start with "¬", and so structural induction finishes it, or both y0,y1 start with "(", and so by the lemma we get contradiction.
@MatheinBoulomenos @LeakyNun: I should add that unique parsing is a key property of a practical formal system, and being prefix-free (no valid expression is a strict prefix of another) is not. For instance, we can omit some brackets if we impose operation precedence, and it will not only be user-friendly but also still satisfy unique parsing (of course different from the one stated above), despite not being prefix-free.
The general kind of unique-parsing property is usually best expressed as a mapping from valid expressions to parse-trees, which will work for any practical formal system, but can be quite irritating. In the case of systems using operation precedence, this mapping directly entails unique-parsing, so it may seem like we are getting something for free. Sort of! What we don't automatically get is the ability to form compound expressions that are parsed as expected.
For example, given formula x,y we want to be able to (computably) construct a formula z that is true iff x,y are both true, and false otherwise. We can do so in the obvious way, namely "("+x+")∧("+y+")", but then we need to prove that it works, which boils down to something similar to what your exercise is asking you to prove.
The reason for this general approach is simply that it applies to real practical formal systems. No published mathematics paper ever uses strict syntactic rules as put forth in an introductory logic textbook; you see "1+2·3+4" instead of "+(+(1,·(2,3)),4)", and this is valid due to infix syntax and operation precedence.
