@article{BarCorGreHerSac08,
  author      = {Bruno Barras and Pierre Corbineau and Benjamin
                 Gr{\'e}goire and Hugo Herbelin and Jorge Luis Sacchini},
  title       = {A New Elimination Rule for the Calculus of Inductive
                 Constructions},
  editor      = {Stefano Berardi and
                 Ferruccio Damiani and
                 Ugo de'Liguoro},
  booktitle   = {Types for Proofs and Programs,
                 International Conference,
                 TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected
                 Papers},
  publisher   = {Springer},
  series      = {Lecture Notes in Computer Science},
  volume      = {5497},
  year        = {2009},
  isbn        = {978-3-642-02443-6},
  pages       = {32-48},
  ee          = {http://dx.doi.org/10.1007/978-3-642-02444-3_3},
}