A compact kernel for the calculus of inductive constructions