CTL is expected to be removed early on

Create pattern-matching cases for all CTL language elements and raise an
error if encountered. We are assuming that CTL is replaced by plain
μ-Calculus early on