Let G4' be a sequent calculus G4 for classical logic with the addition of the following pair of "left" and "right" cut rules:
Let now be G4'' a second calculus G4 for classical logic with the addition of the following "general" cut rule:
I am trying to prove the equivalence between the two calculi G4' and G4''. It is immediate to prove that a sequent derived in G4' can be derived in G4''. About the converse implication, I think it should be possible to prove it by induction on the level of the cut rule (much like a cut elimination proof), but I was wondering if there is a more immediate way to show that any derivation with the "general" cut rule can be rewritten in a derivation that uses the "left" and "right" versions. Does anybody have a suggestion?