This technical report contains the full type-safety proof for the language presented in the paper \emph{Existential Types for Imperative Languages}, originally submitted for publication in October 2001. Because this report should be read only after the paper, effectively as an appendix, we do not repeat the motivation, examples, and informal presentation contained there. Also refer to the paper for related work and a bibliography. We do repeat the figures and definitions so that this report comprises a self-contained proof.