When Gentzen introduced the sequent calculus LK in [19] he also provided a method for the algorithmic elimination of cut inferences from proofs. While there are many important colloraries to a cut-elimination theorem for a calculus such as the consistency of a system, we focus on one particular corollary with applications in proof minining, which Gentzen called the midsequent theorem. This theorem directly corresponds to Herbrand’s theorem [24] and provides the basis for many methods of proof analysis.