This is very different to shadowing where there is a clear scope to the rebinding. In this case, I cannot employ equational reasoning within a scope but must instead trace back through every intervening statement in the scope to check whether the variable is rebound.
It's a straightforward syntactic transformation. The two are equivalent. The scope of the rebound variable begins at the rebinding and ends when the surrounding scope ends. Perfectly clear - the only difference is a "let" keyword.
counter = 0
...
counter = counter + 1
...
vs
let counter = 0 in
...
let counter = counter + 1 in
...
The ellipses in your straightforward transformation are doing some heavy lifting there. Typically the let…in construct has some way to indicate where the scope of the “in” part ends: indentation (Haskell), explicit “end” marker (SML) etc. Even with that, shadowing does make equational reasoning harder (you have to look at more surrounding context) and should generally be avoided.
Sure, scopes are not as easily syntactically visible, but each assignment is creating a new scope, that doesn't change anything for equational reasoning which has to account for captures / substitutions anyways.
No, it’s rebinding the variable within the same scope. Even if you view it as implicitly creating a new scope, the implicit part means it can happen on any line so you have to scan them all and mentally keep track of what changes where, (almost) exactly as you would for imperative code.