Dragalin in his book on Mathematical Intuitionism has given an
outline proof of the admissibility of Contraction and Cut for the
multi-succedent intuitionistic sequent calculus.
One can give a corresponding (but simpler) proof for the
single-succedent calculus. These proofs are given here in
detail as a basis for
extension and modification elsewhere.