[FEATURE] Translate `\E x \in STRING: P` and `\A x \in STRING: P`

[konnov]

It should be quite easy to translate Skolem(\E x \in STRING: P) by introducing an uninterpreted constant. In the more general case, we can use SMT quantifier, which should work reasonably well with uninterpreted constants.