U. Kohlenbach, “A Note on Spector’s Quantifier-Free Rule of Extensionality”, BRICS, vol. 6, no. 20, Jan. 1999.