Fix pretty-printing of {} with Unicode off.

Requires a moderately substantial re-organisation of LVTermNet; this code
is now explicitly a map from keys (terms) to multiple possible forms
underneath. Its interface suggested this anyway, but the implementation
actually only mapped from a term to one possible printing form. This meant
that when a printing form was removed (as when switching Unicode off, which
removed the Unicode symbol as the form for {}), there was nothing left for
the term to map to, even though we'd earlier mapped term EMPTY to string
EMPTY.

A first-order net with support for fixed variables in patterns. These
are variables that mustn't be changed by instantiation.