I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable)
The cases when we consider proof trees for $\Gamma \vdash \phi$ for all rules but and-elimination/if-elimination I don't encounter any difficulty with as the inductive hypothesis (on the weight of proof tree) can be straightforwardly applied, but when the proof tree is that of and-elimination (say), the parent of the consequent may have occurrences of the variable $x$. To make matters worse I couldn't eliminate the problem by attempting to use the induction hypothesis with a 'fresh' variable $m$ replacing all occurrences of $x$ in the parent of the consequent since all such occurrences may be bound.
Any help with this matter would be much appreciated.