Induction Principles Formalized in the Calculus of Constructions