Good description of Calculus of Inductive Construction I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book).

The thing I am interested the most are not definitions but the proofs of important properties.
You can try the Coq user manual, in particular this section is pretty nice (the server seems to be down at the moment though).

For meta-theory you can try some recent work of Benjamin Werner et al., see Proof-irrelevant model of CC with predicative induction and judgmental equality
 and On the strength of proof-irrelevant type theories for the most salient work.