improved typing of bound variables; added support for user-provided Lemmas encoded to the solver; format.fst goes through