Every local declaration has an initialiser, by the grammar. It allocates a fresh location and extends \rho for the following commands. With auto, \tau is the type of the initialiser.

\dfrac{\Gamma \vdash e : \tau \qquad \tau \neq \mathsf{void}}{\Gamma \vdash \tau\ x = e \dashv \Gamma[x \mapsto \tau]}\;\textsf{(T-Decl)}

\dfrac{\Gamma \vdash e : \tau \qquad \tau \neq \mathsf{void}}{\Gamma \vdash \mathtt{auto}\ x = e \dashv \Gamma[x \mapsto \tau]}\;\textsf{(T-Auto)}

\dfrac{\rho, \sigma \vdash e \Rightarrow v, \sigma' \qquad (\ell, \sigma'') = \mathrm{alloc}(\sigma', v)}{\rho, \sigma \vdash \tau\ x = e \Rightarrow \mathsf{normal}, \rho[x \mapsto \ell], \sigma''}\;\textsf{(Decl)}

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.