Proof for $\lor$ Elim: rule in Soundness Theorem So far I have been told to assume the line is invalid and then arrive at a contradiction.
Suppose the first invalid step derives the sentence $C$ by an application of $\lor$ Elim to the sentences $A\lor B$ and $A$ and $B$ appearing earlier in the proof. Let $P_1,\ldots,P_n$ be a list of all the assumptions in force at $C$. If this is an invalid step, $C$ is not a tautological consequence of $P_1,\ldots,P_n$.
Since $C$ is the first invalid step in $p$, we know that $A\lor B$, $A$ and $B$ are all valid steps, that is, they are tautological consequences of the assumptions in force at those steps. 
Since $\mathcal{F}_T$ allows us to cite sentences only in the main proof or subproofs whose assumptions are still in force, we know that the assumptions in force at steps $A\lor B$, $A$ and $B$ are also in force at $C$. Hence the assumptions for those steps are among $P_1,\ldots,P_n$.
But I'm not sure how to carry this on...
 A: Sketch of the proof
We have a derivation $\mathcal D$ of $A \lor B$ with assumptions in $\Delta$.
We have a derivation $\mathcal D_1$ of $C$ from $A$ with assumptions in $\Delta_1$ and a derivation $\mathcal D_2$ of $C$ from $B$ with assumptions in $\Delta_2$.
Let $\mathfrak A$ a model of $\Delta \cup \Delta_1 \cup \Delta_2$.
By induction hypothesis : $\Delta \vDash A \lor B$.
Two subcases : either $\mathfrak A$ is a model of $A$ or it is a model of $B$.
In the first subcase by induction hypothesis ($\Delta_1 \vDash C$) $\mathfrak A$ is a model of $C$.
In the second subcase by induction hypothesis ($\Delta_2 \vDash C$) $\mathfrak A$ is again a model of $C$ .
In both cases $\mathfrak A$ is a model of $C$.
A: There's no compelling reason to use proof by contradiction.  The rule consists of a valid one in intuitionstic positive logic, so like anything else in intuitiionistic positive logic it can get proved without the use of proof by contradiction. 
Suppose that (A $\lor$ B) is true, (A$\rightarrow$C) is true, and (B$\rightarrow$C) is true also.  By the truth table for (A $\lor$ B) one of two cases gets satisfied.  A holds true consists of one case, and B holds true for the other case.  Suppose that A holds true.  Then, by modus ponens C will follow.  Similar reasoning shows that C holds for the other case.  Since that exhausts all cases, C follows from the set of premises.
Note the above does NOT use $\lor$ in the reasoning.  $\lor$ consists of an objective level construct, and is not as comprehensive as meta-linguistic case exhaustive analysis, since case exhaustive analysis could have many more cases than two, while $\lor$ as an objective level connective, defined by the definition of a well-formed formula, consists of a binary connective.
