Støvring, K. Extending the Extensional Lambda Calculus With Surjective Pairing Is Conservative. BRICS 2006, 13.