K. Støvring, “Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative”, BRICS, bd. 12, nr. 35, nov. 2005.