Is $A \& B \multimap A$ derivable? Intuitively, the sentence $A \& B \multimap A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any way to derive it from the definition of $\&$. Is it possible to establish this in linear logic? Or, if not, what makes this sentence different from the definition of $\&$?

It turns out that $A \& B \multimap A$ is provable. Here is the proof, or at least my best attempt at writing it:
$$\DeclareMathOperator{\par}{\unicode{8523}}
\cfrac
{\cfrac
 {\cfrac
  {init}
  {\vdash A^\bot \par A}}
 {\vdash (A^\bot\oplus B^\bot) \par A}}
{\vdash A \& B \multimap A}$$
Using a similar method, you can also prove $A \multimap A\oplus B$.
