### Free Variables Calculation in the `Term_ds` Module

In the `Term_ds` module `term`
type has a field for storing the set of free
variables. This field is supposed to be either `VarsDelayed` if the set
was not computed yet or `(Vars s)` where `s` is the set variable names
(strings) of
all first-order variables occurring free in the term.

The rules for calculating free variables sets are simple:

- Free variables set of an ordinary term is a union of the free variables of
its
`term_terms`
- Free variables set of an ordinary
`bound_term`
contains all variables of
its `bterm` excepts for those that become bound in this `bound_term` (its `bvars`).
- Free variables set of a
`(FOVar v)` is a singleton set consisting of `v`.
- Free variables set of a substitution is equal to the free variables set
of the result of this substitution (see also Note 2)

**Example**:
`x.(x=y)" :`

{ free_vars = {"y"}; core = Term
{ opname = "exists"; term_terms =
[ { bvars = "x"; bterm =
{ free_vars={"x","y"}; core = Term
{ opname = "equal"; term_terms =
[ { bvars = []; bterm =
{ free_vars = {"x"}; core = FOVar "x" } } };
{ bvars = []; bterm =
{ free_vars = {"y"}; core = FOVar "y" } } ] } } } ] } }

(Here "`opname = ...`" is used as an abbreviation for
"`term_op = {op_opname = ...; op_params = []}`" )
Notes:

`Term_ds` tries to distinguish a first-order variable "x" (has a free occurrence
of "x") and 0-ary second-order variable "x" (does not have any free variables).
FO variable "x" is represented as a "special" term (`core = FOVar `"x") while
SO variable "x" is represented as a "usual" term (`core = Term t`, where `t`
is a term with `opname` "var", parameter (`Var `"x") and no subterms)

Since both are indistinguishable in the `Term_std`, sometimes `Term_ds` would use
FOVar "x" (and consider it a free occurrence of "x") when "x" is actually an SO
variable.

When the `Subst` is created, we first remove all "garbage" from the substitution
making sure that all variables that are being substituted for actually occur
in the term. That makes computing the free variables set of the substitution easier and prevents
us from unnecessary duplication of terms.