Prove $Q \vdash [\forall x < \overline{n+1}]\phi \leftrightarrow [\phi^x_{\overline{n}}\land(\forall x <\bar{n})\phi]$ 
Prove that $Q \vdash [\forall x < \overline{n+1}]\phi \leftrightarrow [\phi^x_{\overline{n}}\land(\forall x <\bar{n})\phi]$ where $Q$ is the Robinson Arithmetic, $\phi$ is a formula with single free variable $x$, and $\bar{n}$ denotes $S\cdots S(0)$ ($n$ times $S$).

I can certainly show that $Q \vdash x< \overline{n+1} \leftrightarrow (x<\bar{n} \lor x=\bar{n})$ using one of the axioms of Robinson Arithmetic ($\forall v_1 \forall v_2 (x<Sv_2 \leftrightarrow (v_1<v_2 \lor v_1=v_2))$, but I can't proceed anymore.
 A: First part:
1) $\forall x \ ((x < (n+1)) \to \phi)$ --- premise
2) $(x < (n+1)) \to \phi$ --- from 1) by $\forall$-elim
3) $x < n$ --- assumed [a]
4) $x < (n+1)$ --- from 3) by $\lor$-intro and your equivalence
5) $\phi$ --- from 4) and 2)
6) $(x < n) \to \phi$ --- from 3) and 5) by $\to$-intro, discharging [a]
7) $\forall x \ ((x < n) \to \phi)$ --- from 6) by $\forall$-intro
8) $(n < (n+1)) \to \phi^x_n$ --- from 1) by $\forall$-elim
9) $\mathsf Q \vdash n < (n+1)$
10) $\phi^x_n$ --- from 9) and 8) by modus ponens

11) $\phi^x_n \land \forall x \ ((x < n) \to \phi)$ --- from 7) and 10) by $\land$-intro.


Second part:
1) $\phi^x_n \land \forall x \ ((x < n) \to \phi)$ --- premise
2) $\phi^x_n$ --- from 1) by $\land$-elim
3) $\forall x \ ((x < n) \to \phi)$ --- from 1) by $\land$-elim
4) $(x < (n+1))$ --- assumed [a]
5) $x < n \lor x=n$ --- from 4)
Now a proof by cases ($\lor$-elim) deriving $\phi$ under both braches: $x=n$ and $x < n$:
6) $\phi$
7) $(x < (n+1)) \to \phi$ --- from 4) and 6), discharging [a]

8) $\forall x \ ((x < (n+1)) \to \phi)$ --- from 7) by $\forall$-intro.

A: Note that $[\forall x < \overline{n+1}]\phi$ is a shorthand for $\forall x (x < \overline{n+1} \to \phi)$, which is equivalent to  $\forall x ((x = \overline{n} \lor x < \overline{n}) \to \phi)$, as you correctly remarked. 
Now, observe that $\forall x ((x = \overline{n} \lor x < \overline{n}) \to \phi)$ is equivalent to $\forall x ((x = \overline{n} \to \phi) \land (x < \overline{n} \to \phi))$, because in propositional logic $(A \lor B) \to C \equiv (A \to C) \land (B \to C)$.
Since in first-order logic $\forall x (A \land B) \equiv \forall x A \land \forall x B$, then $\forall x ((x = \overline{n} \to \phi) \land (x < \overline{n} \to \phi))$ is equivalent to $\forall x (x = \overline{n} \to \phi) \land \forall x(x < \overline{n} \to \phi)$, which is equivalent to $\phi_\overline{n}^x \land \forall x(x < \overline{n} \to \phi)$.
