  Some quantitative results obtained by proof mining take the form of Herbrand
disjunctions that may depend on additional parameters. We attempt to elucidate
this fact through an extension to first-order arithmetic of the proof of
Herbrand's theorem due to Gerhardy and Kohlenbach which uses the functional
interpretation.
