The main concern of this paper is the design of a noetherian and confluent normalization for $\mathbf{LK}^2$ (that is, classical second order predicate logic presented as a sequent calculus). The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's $\mathbf{LC}$ and Parigot's $\lambda\mu, \mathbf{FD}$ ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding $\mathbf{LK}$ into $\mathbf{LJ}$ (intuitionistic sequent calculus) brings to the fore the latter's defects for these `deconstructive purposes'.