 We can now formulate the desired →-introduction rule so that the assumption discharge feature is visible in what happens on the left of the sequent-separator as we move from premiss-sequent to conclusion-sequent. We write the elimination rule alongside in a similar notation; included also are the natural deduction rules for ∨; the earlier rules for ∧ should be imagined as re-written along similar lines, with assumption-dependencies made explicit: