Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\Lambda X_2.\dots.\Lambda X_n.\lambda x:U.t)$ is a function of type $\forall \vec{X}.U\to T$ and we want to apply it to an argument of type $V$. Then we need to find types $W_1,\dots,W_n$ such that $U[\vec{X}/\vec{W}]=V$.
This is clearly another unification problem. Can we solve this problem as easily as the problem with one variable? What is the algorithm for doing this?