Gerhardy, P., and U. Kohlenbach. “Extracting Herbrand Disjunctions by Functional Interpretation”. BRICS Report Series, vol. 10, no. 32, Oct. 2003, doi:10.7146/brics.v10i32.21800.