K. Støvring, “Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative”, BRICS, bd. 13, nr. 5, mar. 2006.