Ambient Calculus and its Logic in the Calculus of Inductive Constructions