Lambda Calculus and Surjective Pairing
Here is a formal proof that
extending the extensional lambda calculus
with surjective pairing is conservative. The proof is written using
version 1.5R1 of the Twelf system.
The proof is from the article:
Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective
Pairing is Conservative.
Logical Methods in Computer Science, 2(2:1):1-14,
March 2006.