On the role of type decorations in the calculus of inductive constructions

In proof systems like,Coq [161, proof-checking involves comparing types modulo beta-conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also e rased. It generalizes and strengthens significantly a similar result by Barthe and Sorensen [5] on the class of functional Domain-free Pure Type Systems.