The statement "proving a variable is never used" is not fully specified. What does it mean for it to not be used? (Or rather, not be used again?). One way to in

The statement "proving a variable is never used" is not fully specified. What does it mean for it to not be used? (Or rather, not be used again?). One way to interpret it (which I think is the one you used) is that at runtime it will no longer be read/wrote. Another one is to that it is no longer syntactically referenced, which is much easier to reason about and statically prove.