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.