Just reproducing the theorem in a larger size:
.
Is that correct?
Question: does the initial for all x apply to the entire disjunct before the symbol?
I'm afraid I can't be of much more use than this. Herbrand's theorem is beyond what I've done in logic.
When you say "use Herbrand's theorem" do you mean that you need to perform this proof in some particular kind of sequent calculus?
Otherwise, in ordinary natural deduction, a proof is easy:
Suppose x is not 0 nor the successor of 0. Then there is a z such that x is the successor of z. But such z is itself either 0 or a successor. But z can't be 0, since x is not the successor of 0. So let z be the successor of y. So x is the successor of the successor of y. Then fill out the routine quantifer and sentential logic steps to complete the proof.