# Proving Negation Identity in Intuitionistic Linear Logic

In a Gentzen system (i.e. sequent calculus) for Intuitionistic Linear Logic (from now, ILL), given the usual rules for ILL ($\wedge L, \wedge R, \circ L, etc.$), I want to prove that the Identity $A \vdash A$ may be proved from the instances of identity using atomic propositions alone.

It follows a proof on the complexity of formulas. For $Conjunction$ we have:

$\quad A\vdash A \qquad B\vdash B$

$———————————— \; [\wedge L]$

$A\wedge B\vdash B\qquad A\wedge B\vdash B$

$———————————— \; [\wedge R]$

$\qquad A\wedge B\vdash A\wedge B$

The rules for $Negation$ are the following two:

$X \vdash A$

$———————————— \; [\neg L]$

$X; \neg A \vdash$

$\;$

$X; A \vdash$

$———————————— \; [\neg R]$

$X \vdash \neg A$

So, my proof (and my problem) in this case is:

$\;$

$A \vdash A$

$———————————— \; [\neg L]$

$A; \neg A \vdash$

$———————————— \; [??]$

$\neg A; A \vdash$

$———————————— \; [\neg R]$

$\neg A \vdash \neg A$

$\;$

Where I put the question marks is the line that I find problematic. Am I allowed to assume some sort of structural commutativity or exchange in ILL?

Thanks.