 All the connectives of the standard sequent calculi, including the cases of classical and intuitionistic linear logic, are inserted by rules which are both Id-inductive and Cut-inductive, as we illustrate here with the rules for →. For definiteness, think of these as the Left and Right rules of classical linear logic. To show Id-inductivity, we must show that φ → ψ ≻ φ → ψ is provable using the → rules, given (‘the inductive hypothesis’) that φ ≻ φ and ψ ≻ ψ are. (We write φ and ψ rather than φ1 and φ2.) From the last two sequents, (→ Left) delivers: φ → ψ, φ ≻ ψ. From this an application of (→ Right) gives the desired conclusion: φ → ψ ≻ φ → ψ.