K. Støvring, “Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative”, BRICS, vol. 13, no. 5, Mar. 2006.