I have been reading Florian Steinberger's PhD thesis on harmony in sequent calculus, when he asserts that the left-intro rule is functionally equivalent to elimination rule.
His argument is attached at the bottom, but there are two things I don't understand:
Why is $C$ being provable from $\Gamma, A\land B$ a fortiori? $\{\Gamma, A\land B\}$ is not really a stronger set of premises than $\{\Gamma, A\}$, since the latter can be strengthened to the former by left-$\land$ rule, but the former cannot revert back to the latter. In other words, it would seem that the former can prove less than the latter. So why is it a fortiori/for a stronger reason?
Why is the upward extension (at the end of quotation) a justification of the two being functionally equivalent? I don't at all understand what he is trying to do with the last natural deduction ($\land$ elimination).
You can say that the hypothesis $\Gamma, A \land B$ is stronger than $\Gamma, A$ because in $\Gamma, A \land B$ you have more hypotheses than in $\Gamma, A$. But the statement $\Gamma, A \land B \vdash C$ (i.e. $C$ is derivable from the hypotheses $\Gamma, A \land B$) is weaker (in the sense of less general or less informative) than the statement $\Gamma, A \vdash C$ (i.e. $C$ is derivable from the hypotheses $\Gamma, A$). The latter statement means that actually the hypothesis $B$ is not needed to derive $C$ from $\Gamma, A$. So, if you can derive $C$ from $\Gamma, A$, then a fortiori you can derive $C$ from $\Gamma, A$ plus another hypothesis ($B$) that actually is not needed.
Technically, the issue is to show that any derivation in sequent calculus can be translated into a derivation in natural deduction, with the same conclusion and the same hypotheses. This translation is defined by induction on the size of the derivation in sequent calculus that has to be translated. Let us consider the case of the following derivation in sequent calculus (whose last rule is a left introduction of the conjunction): \begin{align}\tag{1} \dfrac{\quad \Pi \\ \Gamma, A \vdash C}{\Gamma, A \land B \vdash C} \land_{L_1} \end{align} By induction hypothesis applied to the derivation $\Pi$ (whose conclusion is $\Gamma, A \vdash C$), there is a derivation in natural deduction \begin{align} \Gamma, A \\ \vdots \Pi_0 \\ \!\!\!\!\!\!\!\!\!C \end{align} But if we add an elimination rule for the conjunction above $A$, we get the following derivation in natural deduction \begin{align} \Gamma,& \dfrac{A \land B}{A}\land_{E_1} \\ &\vdots \Pi_0 \\ &C \end{align} which is the translation of the derivation $(1)$ into natural deduction, with the same conclusion and hypotheses. In this sense, the introduction rule for the conjunction in $(1)$ corresponds to an upward extension of the derivation in natural deduction beginning with an elimination rule for the conjunction.
EDIT: Context and Preliminaries for the Two Questions.
I guess the context of what Streinberger wrote is to show the equivalence (or ''coextensivenes'') of natural deduction and sequent calculus: every proof in the former system can be translated into a proof in the latter formalism, with the same hypotheses and conclusion, and vice versa. In particular, the passage you cited is about the translation of a sequent calculus derivation into a natural deduction derivation. To be precise in the statement that you want to prove, you have to take into account a difference between sequent calculus and natural deduction: inference rules in natural deduction have an effect on formulas, whereas inference rules in sequent calculus have an effect on sequents, which are pairs of the form $\Gamma \vdash A$ where $A$ is a formula and $\Gamma$ is a sequence or multiset of formulas. For instance, look at the difference between the left rule for conjunction in the sequent calculus ($\land_{L_1}$) and the elimination rule for the conjunction in the natural deduction ($\land_{E_1}$, see above).
So, a derivation in natural deduction has the form \begin{align}\tag{2} \Gamma \\ \vdots \\ A \end{align} where $\Gamma$ is the set of undischarged hypotheses (roughly, the top formulas in the derivation), and $A$ is the conclusion (the bottom of the derivation).
A derivation in the sequent calculus has the form \begin{align}\tag{3} &\vdots \\ \Gamma &\vdash A \end{align} where the sequent at the bottom of the derivation contains both the hypotheses $\Gamma$ and the actual conclusion $A$.
Thus, in the passage you cited, Streinberger aims to prove that every sequent calculus derivation of the form $(3)$ can be translated into a natural deduction derivation of the form $(2)$ (in the passage you cited he does not consider the vice versa, I suppose he deals with it somewhere else). The idea of the proof is to define a rule-by-rule translation, i.e. to show that every inference rule in the sequent calculus can be translated into one or more inference rules in the natural deduction. This translation is quite easy to define for the right rules in the sequent calculus, since their behavior is analogous to the introduction rules in the natural deduction. The translation of the left rules in the sequent calculus is more delicate, since in the natural deduction apparently there are no similar rules. As shown by Steinbergerer in the case of conjunction (see above), the idea is that left rules in the sequent calculus modify the part of hypotheses in a sequent, so they can be simulated in the natural deduction by elimination rules.