Invertibility of inference rules with quantifiers

Question

In the $LK$ system for sequent calculus, the inference rules with quantifiers are four: $\forall R$, $\exists L$, $\forall L$ and $\exists R$. In the course we specified that the first two are invertible, and the last two are not (because, clearly, when you apply those rules from bottom to top, you "lose some informations"). Now, in order to maintain the invertibility, the professor said that one should use contraction, and then apply one of the non invertible rules. My question is: if one applies $\forall L$ or $\exists R$ substituting a variable not used before (so basically if one apply the non invertible rules with the same restrictions that are used for the invertible ones), do those rules become invertible too?

Answer 1

No; for example, let $a,b$ be two distinct variables and $P$ a unary predicate. Then the $(\forall L)$ inference $$ { P(a)\vdash P(b) \over \forall x P(x) \vdash P(b) } $$ satisfies the eigenvariable condition ($a$ does not occur freely in the lower sequent) and its conclusion is valid, while its premise clearly is not.