Extending the lambda calculus with surjective pairing is conservative

Consideration is given to the equational theory λπ of lambda calculus extended with constants π, π₀, π₁ and axioms for subjective pairing: π₀(πXY)=X, π₁(πXY)=Y, π(π₀X )(π₁X)=X. The reduction system that one obtains by reading the equations are reductions (from left to right) is not Church-Rosser. Despite this failure, the author obtains a syntactic consistency proof of λπ and shows that it is a conservative extension of the pure λ calculus