Automatic proofs for implications 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
Merge branch 'develop' of github.com:hbr/modern-eiffel into develop

Corrected a typo and commited with amend after pushing to the remote repo.