The most significant difference between Gentzen's original calculus and the way it is most often given today is that discharge of assumptions are associated wit

The most significant difference between Gentzen's original calculus and the way it is most often given today is that discharge of assumptions are associated with labels in modern calculus, so each discharged assumption is tied to a rule, whereas in Gentzen's calculus, all instances of that proposition are discharged. The innovation is essential to the Curry-Howard correspondence, because this labelling of assumptions matches variable bindings in typed lambda calculus.