symbols are automatically interned by term constructors;
higher order representation of terms (const/var/apply of term * term list) that should be more flexible
to encode higher order constructs, or to encode types in terms...