  Herbrand's theorem is one of the most fundamental insights in logic. From the
syntactic point of view, it suggests a compact representation of proofs in
classical first- and higher-order logic by recording the information of which
instances have been chosen for which quantifiers.
  This compact representation is known in the literature as Miller's expansion
tree proof. It is inherently analytic and hence corresponds to a cut-free
sequent calculus proof. Recently several extensions of such proof
representations to proofs with cuts have been proposed. These extensions are
based on graphical formalisms similar to proof nets and are limited to prenex
formulas.
  In this paper we present a new syntactic approach that directly extends
Miller's expansion trees by cuts and covers also non-prenex formulas. We
describe a cut-elimination procedure for our expansion trees with cut that is
based on the natural reduction steps and show that it is weakly normalizing.
