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 $\&$?

$\DeclareMathOperator{\par}{\unicode{8523}}$
Yes, $A \& B \multimap A$ is provable in linear logic sequent calculus, but the derivation in the answer above is wrong, because there is no rule that allows one to derive $\vdash (A^\bot\oplus B^\bot) \par A$ from $\vdash A^\bot \par A$ (an inference rule in the sequent calculus can only introduce a new principal connective in a formula).
A correct derivation of $A \& B \multimap A$ in the one-sided sequent calculus for linear logic is below.
Note that, according to the one-sided formulation, $A \& B \multimap A$ is the same formula as $(A^\bot\oplus B^\bot) \par A$.
\begin{align}
 \dfrac{\dfrac{\dfrac{}{A^\bot, A}\text{ax}}{A^\bot \oplus B^\bot, A}\oplus}{(A^\bot \oplus B^\bot) \par A} \par
\end{align}
