K. Støvring, “Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative”, BRICS, vol. 12, no. 35, Nov. 2005.