Pierre-Louis Curien, Roberto Di Cosmo: A Concluent Reduction for the Lambda-Calculus with Surjective Pairing and Terminal Object. ICALP 1991: 291-302