I think that there is no "compact" formalization of the required double substitution.
Assuming that [using $v_0, v_1, v_2$] :
$\varphi (v_1) := \forall v_0 \psi(v_0, v_1)$
we have :
$\forall v_0 \psi(v_0, v_1)[v_0 ← v_2] \equiv \forall v_2 \psi(v_2, v_1)$
with $v_2$ a new variable. This condition licences us to prove the equivalence.
Now we can perform the second substitution :
$\varphi (v_0) := \forall v_2 \psi(v_2, v_1)[v_1 ← v_0]$.
But, in general :
$\varphi(v_1) \nvdash \varphi(v_0)$.
We can try with the approach to substitution in John Bell & Moshe Machover, A Course in Mathematical Logic (1977), page 57-on.
The "syntax" for substitution is : $\alpha(x,t)$ and the basic defintion is Definition 3.3 [page 59] :
We shall say that $t$ is free to be substituted for $x$ in $\alpha$ (briefly, free for
$x$ in $\alpha$) if no free occurrence of $x$ in $\alpha$ is within a subformula of $\alpha$ having the form $\forall y \beta$ where $y$ occurs in $t$.
If $t$ is free for $x$ in $\alpha$, we shall define $\alpha(x/t)$ as the result of substituting an occurrence of $t$ for each free occurrence of $x$ in $\alpha$.
Definition 3.5 [page 61]. If $z$ is a variable which is not free in $\beta$ but is free for $x$ in $\beta$, we say that $\forall z [\beta(x/z)]$ arises from $\forall x \beta$ by (correct) alphabetic change. (Note that if $z$ does not occur at all in $\beta$, then $z$ certainly satisfies both of the above conditions.)
Thus, considering again the formula :
$\varphi := \forall v_0 \psi(v_0, v_1, v_2)$
we perform an alphabetic change using $v_n$, where $v_n$ is the first variable not occurring in $\varphi$, getting :
$\forall v_n [\psi(v_0/v_n, v_1, v_2)]$
and then the substitution : $v_1 ← v_0$ (now $v_0$ is free for $v_1$ in the formula), to get :
$\forall v_n [\psi(v_0/v_n, v_1/v_0, v_2)]$.
The result will be :
$\varphi' := \forall v_n \psi(v_n, v_0, v_2)$.