  In recent years, a great deal of work has been done on the proof theory of classical logic, inspired and informed by research into substructural logics. Classical logic has the full complement of structural rules, and is historically prior to more recent systems of substructural logics. However, when it comes to attempting to understand the deep structure of classical proof systems (and in particular, when two derivations that differ in some superficial syntactic way are really different ways to represent the one underlying ‘proof’) it is enlightening to think of classical logic as formed by a basic substructural logic, in which extra structural rules are imposed as additions. In particular, it has become clear that what distinguishes classical proof from its siblings is the presence of the structural rules of contraction and weakening in their complete generality (see, for example, Bellin et al. 2006 and the literature cited therein).