Formalizing a lazy substitution proof system for μ-calculus in the Calculus of Inductive Constructions