more recent Sequence module
removed redundant function in Term;
more elaborate type inference, and helpers in Util_tptp