Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini. A New Elimination Rule for the Calculus of Inductive Constructions. In Stefano Berardi, Ferruccio Damiani, Ugo de Liguoro, editors, Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers. Volume 5497 of Lecture Notes in Computer Science, pages 32-48, Springer, 2008. [doi]
Abstract is missing.