Admissibility of structural rules for contraction-free systems of intuitionistic logic

We give a direct proof of admissibility of cut and contraction for the cont raction-free sequent calculus G4ip for intuitionistic propositional logic a nd for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other. indirect, proofs. i.e .. those which use induction on sequent weight or appeal to admissibility o f rules in other calculi.