-->

Completeness and Decidability Results for CTL in Coq