Is the proof of the assume thattemp doesn't alias inputwrong in section 3.2

[yejunjin]

The doc says:

We're still relying on alias analysis to assume that temp doesn't alias input, but the proof is much simpler: the value of a local variable can't be aliased by things that existed before it was declared. This is an assumption every language freely makes, and so this version of the function could be optimized the way we want in any language.

The assumption is that temp doesn't ALIAS input, but the proof is try to prove input doesn't ALIAS local variable temp.