This technical report presents the full proofs for the type preservation and effect soundness theorems of the type system presented in the article "Lightweight Polymorphic Effects".