  Analogous rules permit weakening and contraction in the right,  succedent parts of sequents. Weakening is made an eliminable rule by  letting initial sequents have the form  A, Γ → Δ, A  instead of Gentzen's  A → A. Contraction is likewise made  eliminable by a suitable formulation of the rules. The import is that in root-first proof search, no rules need be applied that would  produce a duplication of a formula in a premiss. Without this result, non-termination of proof search would not follow.