Herbelin's Calculus of Explicit Substitutions as a Sequent Calculus Isomorphic to Natural Deduction Interest in traditional proof theory, as a basis for (e.g.) logic programming, led to the consideration of the sequent calculus of Herbelin in which cut-free terms represent normal natural deductions in a bijective fashion. The cut-reduction rules are easily interpreted as ES reduction rules; but as formulated by Herbelin these were not adequate to simulate beta-reduction. We add simple extra rules, allowing such simulation without losing confluence and termination. The calculus can thus be seen as a system, with roots in Gentzen-style proof theory, for representing lambda-terms with explicit substitutions.