P. Gerhardy and U. Kohlenbach, “General Logical Metatheorems for Functional Analysis”, BRICS, vol. 12, no. 21, Jul. 2005.