Support parsing infix functions AND infix predicates

Created by: cache-nez

To do so, introduce Termula type, which doesn't distinguish function application from predicate application. A string is parsed into a Termula, which then gets converted into a Formula or a Term, with the appropriate checks.

Telling apart infix function and predicate application in LL1 parser does not appear feasible: consider two inputs, (x + y) < z and (a /\ b) /\ c. The parser is parsing a formula and observes '(' as the first token. It can either mean a subformula or a subterm with an infix operator, and this conflict seems fundamental. With the introduction of Termula, '(' corresponds to a start of subtermula, and the rest of the inputs is parsed either into a connector termula or an (infix) application termula.

Depends on #90. Fixes #75 (more unicode aliases to be added).