The call-by-push-value (CBPV) calculus is a general framework within which one can study computational effects such as state, nondeterminism, and input/output. Compared to the simply typed lambda calculus, the CBPV type system is much more fine-grained and distinguishes between value and computation types. We give a self-contained proof of strong normalization for CBPV, employing a notion of TopTop-closure to adapt the Girard-Tait method to CBPV computation types.