Bugfix: Anonymous variables must be the complement of de Bruijn indices

Internally de Bruijn indices are used as variable names. In an environment with
n anonymous variables we use the names @0, @1, ... @n-1 as external representation
but the corresponding de Bruijn indices are n-1, n-2, ... 0.

	modified:   ocaml/feature_table.ml
Added proof tracing, function expansion and beta reduction

1. Proofs can be traced. There is a trace flag. If it is not set the prover
   starts without tracing. If it cannot proof an assertion it sets the
   trace flag and restarts the proof.

2. Functions can be expanded i.e. all function symbols which have a definition
   are replaced by the corresponding lambda term.

3. Beta reduction means applying all lambda terms to their arguments.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/term.ml