No tabs any more

As there should never be free variables in formulas within the
FL-Closure maybe we should rather signal an error here?

Make following state of a fixpoint it's unfold

should now properly calculate the FL-Closure

previously only late parser steps were used so modalities were allowed
but not e.g. disjunctions. With this change all of the
CTLComparisonBenchmarks formulas successfully parse

Example formulas from the benchmark seem to all have parens so assume
they are there

We need to enforce some assumptions for μ-Calculus. Add (still empty)
checker function and call them when importing the forumla

Add all obvious cases for hcFormula

so it's `MU of string * formula` again. The variable within the formula
is still represented as `VAR s`

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

Needed e.g. to implement the CTL → μ conversion

CTL is assumed to be eliminated before the hash-consing step