Gerhardy, P.; Kohlenbach, U. General Logical Metatheorems for Functional Analysis. BRICS 2005, 12.