Progress on restoring inference soundness proof
Change the determinism check in the type system

For definition val p = e; previously I was checking that there could
only be 1 type for e, but in fact the proper check to line up with what
the inference system does is that there is only 1 possible environment
from p (after ensuring that p and e have the same type).

Check that the type environment of the definition