More work toward sketching out the type inference proof

Got a simple lemma about infer_e to go through (that the next
unification variable to be allocated does not decrease).  So at least
the basic infrastructure should be in place for getting rid of all of
the monadic aspects if infer_e.