(1)
Gerhardy, P.; Kohlenbach, U. Extracting Herbrand Disjunctions by Functional Interpretation. BRICS 2003, 10.