move type system theorems into typeSysPropsTheory

also:

- cheat a case of type_e_closed, which probably changed due to removing
  generalisation of nested lets

- move some definitions of things to do with free variables into
  evalPropsTheory (from free_varsTheory)