P. Gerhardy and U. Kohlenbach, “Extracting Herbrand Disjunctions by Functional Interpretation”, BRICS, vol. 10, no. 32, Oct. 2003.