in terms, mk_var requires a type (does not assume Type.i by default);
mk_bind/mk_forall/mk_lambda etc. also require a type, but BoundVar do not
(put the type in the binder is cleaner);
updated most modules to handle new term/type system