most natural formulation of the $\vee$-eliminating rule There are several (equivalent) ways to formulate the eliminating rule of $\vee$ ("or")
Here are two of them:


*

*$\begin{array}{c}
A\vee B \quad A\vdash C \quad B\vdash C\\
\hline
C
\end{array}$

*$\begin{array}{c}
A\vee B \quad A\rightarrow C \quad B\rightarrow C\\
\hline
C
\end{array}$
My question is: Which variant is the most natural one (in your opinion)?
A disadvantage/detour of the 1. formulation is noticeable when proving the implications by contraposition.
 A: Answer: neither of those is happy.
In a natural deduction framework -- and talk of introduction and elimination rules has its natural(!) home here -- the canonical formulation of $\lor$-elimination looks like this:
$${}\quad \quad \quad [A] \quad \quad \quad [B]\\
\quad \quad \quad \vdots \quad \quad \quad \;\;\vdots\\
(A \lor B)\quad \quad \quad C \quad \quad \quad \;\;C\quad\quad\quad\\
-------------\quad\quad\quad\\
C\quad\quad$$
That is to say, given $(A \lor B)$ and a subproof from the temporary assumption $A$ to $C$ and a subproof from the temporary assumption $B$ to $C$, we can discharge the two temporary assumptions (marking the discharge by square brackets) and infer $C$.
Your first formulation is unhappy as it seems aiming  to be part of a sequent calculus formulation, but all the expressions in a sequent calculus argument have to be sequents, involving $\vdash$ (or whatever your sequent-constructor is). If on the other hand you intend $\vdash$ to be the usual metalinguistic expression for syntactic entailment, then what you have above the line is an unhappy mix of object and metalanguage statements.
Your second formulation is unhappy as we ideally want introduction and elimination for a connective not to involve other connectives (you might not have a conditional primitively available in the language, and if you have introduced $A \to B$ as short for $\neg A \lor B$, you are in trouble!). 
