Completeness and Decidability Results for CTL in Coq