update type erasure so that free type vars can be quantified;
functions to compute the set of free type variables in terms and formulas;
type_check now can print the annotated set of input formulas (function to do that in Util_tptp)