Tweaked TermM to incorporate lambda-bound variables

Also provided an implementation of inferType for Var cases, given this
definition of TermM.