Fix: Calculation of type variables during typing

	modified:   ocaml/context.ml
	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/typer.ml
More functions for focussed expansion prepared

.. but not yet activated

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml
Fix: find_equivalent -> find_stronger

An assertion shall not be entered into the proof tables if there is
an equivalent or stronger assertion already in the context.

An assertion is equivalent or stronger if it has a less or equal number
of variables and the stronger assertion can be transformed into the
weaker assertion by using an injective substitution of the variables.

An assertion is weaker in this sense only if it doesn't use some of its
variables. Such an assertion is usually useless for the prover.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
Allowed more forward reasoning

Before: A forward rule must be either simplifying or and elimination
rule in order to get applied. I.e. only elimination rules are allowed
to increase the node count of a derived consequence.

Now: Some rules are regarded as elimination rules even if the don't
eliminate any symbol. This is the case if an elimination rule is added
by partial specialization. The elimination property carries over to this
partial specialization and to the consequence. The 'elim' flag is resetted
as soon as all variables are substituted.

	modified:   ocaml/proof_context.ml
Focussed expansion activated

	modified:   ocaml/proof_table.ml
	modified:   ocaml/prover.ml