Simplify 3{x}: @{x}: ... classification.

[daemontus]

If a formula starts with the sequence 3{x}: @{x}: ... , this essentially means that the user does not want to assume "universal", but rather "existential" formula validity (i.e. to be satisfied, it does not have to hold in all states, just one state). If x does not appear anywhere else in the inner formula, we can simplify the classification process: Compute all satisfying states, and then perform standard existential projection on the set of colours. This should be much faster, as it does not require allocation of extra HCTL variables.