  In a previous work, we proved that almost all of the Calculus of Inductive
Constructions (CIC), which is the basis of the proof assistant Coq, can be seen
as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of
Constructions with functions and predicates defined by higher-order rewrite
rules. In this paper, we not only prove that CIC as a whole can be seen as a
CAC, but also that it can be extended with non-free constructors,
pattern-matching on defined symbols, non-strictly positive types and
inductive-recursive types.
