Various improvements and refactoring

Created by: SimonGuilloud

-New package utilities containing the KernelHelper and tptp, and suitable for ace. -Theorems now require the target statement (related to https://github.com/epfl-lara/lisa/issues/9) This is still a bit cheaty or cumbersome without a full parser for the kernel. -Various other corrections, merge conflicts resolved... -Keep function and predicate label definitions distinct in the running theory for now, to keep knowledge as much as possible.