Fix substitution in the presence of shadowing global names

[wilcoxjay]

Consider this program

sort s

mutable x: bool

def y() -> bool {
    x
}

assume forall x:s. y

If we call Module::inline_defs on this module it will produce

sort s

mutable x: bool

assume forall x:s. x

which is incorrect (it's not even well sorted!). It should instead produce

sort s

mutable x: bool

assume forall x0:s. x

which is well sorted and intuitively the right answer. Notice that the bound variable had to be renamed to allow the body to refer to the global x after substitution.

---

I'm filing this issue just so we don't lose track of it. I'll assign it to me. I plan to fix it via capture avoiding substitution, but probably not until next week.