Automatic proofs for implication with forward reasoning implemented

The prover can now prove all boolean assertions of the kind

    a=>a
    (a=>b) => (b=>c) => (a=>c)
    (a=>b) => (a=>b=>c) => c

by applying forward reasoning. Endless loops in the closure of the term map are detected.

Backward reasoning is implemented, but endless loop detection still needs to be implemented.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli