 In \(\forall L\) and \(\exists R\), t is an arbitrary term. The variable a in \(\forall R\) and \(\exists L\) is an eigenvariable of the respective inference, i.e., a is not to occur in the lower sequent.