As far as I know, there are only 2 restrictions for the universal introduction rule of inference which are the following:
P[a/x] can become forall x.P if:
1. x is not mentioned in P
2. a is not mentioned in a premise
But these don't prevent the problem mentioned here:
So is the list of restrictions incomplete or is there something I'm missing here?