On the formalization of the modal mu-calculus in the calculus of inductive constructions