Variable bindings in binding operators

[Jazzpirate]

Problem: FLaTeX needs support for binders. Bound variables can represent simple variables (e.g. \sum_{n\in N}n, where N is a "type"), but also sequences (e.g. \forall{x_1,...,x_n}..., see #7) or more complicated patterns (e.g. \sum_{(a,b)\in S}a^2\cdot b^2).

In the latter case, MMT probably has to take care of converting this to something tangible.

Related to #3