 Sequent natural deduction turns out to be very usable in practice. Explicit mention of the structural rules of Interchange and Contraction can be avoided by stipulating that the list of antecedent formulas is simply a representation of a set of formulas. Natural deduction rules with two premisses can be formulated to allow merging of antecedents: thus, for example, \(\rightarrow\)-E should allow the inference of