Elimination of unused variables in assertions

From any assertion unused variables are eliminated. E.g. in partial order we
have the compound assertion which states reflexivity, antisymmetry and
transitivity

     all(a,b,c:PO) deferred ensure
                       a <= a
                       (a <= b) => (b <= a) => (a = b)
                       (a <= b) => (b <= c) => (a <= c)
                   end

From this compound assertion three assertions are generated.

     all(a:PO)     deferred ensure
                       a <= a
                   end

     all(a,b:PO)   deferred ensure
                       (a <= b) => (b <= a) => (a = b)
                   end

     all(a,b,c:PO) deferred ensure
                       (a <= b) => (b <= c) => (a <= c)
                   end

I.e. all unused variables are eliminated.

However it is not always possible to eliminate all unused variables because it
might be the case that unused variables are used within the proof of an assertion.

Example "Impossible object":

     case class VOID end

The class `VOID` has no constructors, therefore it is impossible to construct
an object of type `VOID`. Since the class generates an inductive type, the
compiler generates the corresponding induction principle:

    all(x:VOID, p:VOID?)  p(x)

I.e. all `x` of type `VOID` satisfy any predicate. This is certainly true,
because there are no objects of type `VOID`. I.e. the statement holds
_vacuously_.

Similar to _ex falso_ we can derive anything from the existence of an object
of type `VOID`.

    all(x:VOID)
        proof
            {x:false}(x)    -- induction principle
            false           -- beta reduction
        ensure
            false           -- illegal conclusion
        end

The variable `x` is not used in the assertion. Therefore the prover wants to
eliminate it and generate the assertion `false` which shall never happen.

In order to avoid this illegal conclusion the prover finds out that `x` is
used in the proof but not in the conclusion and rejects the proof.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/term.ml