add support for EQLTL

Read Stutter-Invariant Languages, ω-Automata, and Temporal-Logic.

A basic plan would be:

• Add an ∃ unary operator
• modify the LTL parser to accept ∃ only at the top-level.
• add a function label_filter(tgba_digraph_ptr& aut, bdd vars) that removes all variables in vars from the labels of aut.
• Adjust the translations. To translate ∃(a,b) f(a,b,c,d), first translate f(a,b,c,d), and then apply label_filter to remove a, and b. (Note in Couvreur/FM, removing a,b could be done during the same pass that complements promises.)
• Implement Etessami's conversion from BA to EQLTL.
• Implement a conversion from TGBA to EQLTL.

A more general idea would be to allow ∃ at all level in the formulas, during the translation, we have to apply bdd_exist on the BDD-rewriting of any subformula of a ∃ operator.
Would it be correct to do the same with ∀ and bdd_forall? If that is true, that gives us a conceptually simple way to negate an automaton: translate it to EQLTL, negate it (giving an ∀-quantified LTL formula), and translate it back.