 Suppose that the last rule applied was \((\exists\)E), we have \(\Gamma_3 \vdash \exists v\theta\) and \(\Gamma_4, \theta (v|t) \vdash \phi\), with \(\Gamma_1\) being \(\Gamma_3, \Gamma_4\), and \(t\) not in \(\phi\), \(\Gamma_4\) or \(\theta\). If \(t\) does not occur free in \(\Gamma_2\), we apply the induction hypothesis to get \(\Gamma_2 \vdash \exists v\theta\), and then \((\exists\)E) to end up with \(\Gamma_2 \vdash \phi\). If \(t\) does occur free in \(\Gamma_2\), then we follow a similar proceedure to \(\forall I\), using Lemma 7. 