Gerhardy, P., and U. Kohlenbach. “General Logical Metatheorems for Functional Analysis”. BRICS Report Series, vol. 12, no. 21, July 2005, doi:10.7146/brics.v12i21.21887.