Prenex normalization for universal quantifiers implemented

We use prenex normal form with respect to universal quantification. The
normalization is implemented but not yet used (but partially tested).

E.g. the proved terms

    all(x) all(y) g(x,y)

    all(x) f(x) ==> all(y) g(x,y)

are normalized to

    all(x,y) g(x,y)

    all(x,y) f(x) ==> g(x,y)

This requires that the term and its proof term have to be normalized to be
consistent.

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