support named expressions and syntactic substitution

[johnyf]

For example,

a == ...
b == ... a ...

where the defined symbols are not variables, but simply expressions to be reused throughout.

Similar in purpose and function to the memory buffers of the slugsin format, described here, with the difference that it is simple mathematics, readable, and flat (no nesting and global scope -- which can be both good and bad).

This will allow input of bitblasted formulae from omega, therefore linear arithmetic with quantifiers over rigid variables (otherwise formulae blow up).

Adding syntax for ite would serve a similar purpose, but it wouldn't avoid duplication. Naming can avoid blowup of bitblasted arithmetic formulae.