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.