Can you help me with my approach to the following task:
Define simultaneous substitution $\phi[\psi_1,...,\psi_k/p_1,...,p_k]$ recursively.
Usually we have recursive definitions about formulas, but I think here I have to define it rekursively on k?
base case - $k=1$.
$\phi[\psi_1/p_1] = \phi[\psi_1/p_1]$
recursive case - $k > 1$.
Let $p^'_k$ be a variable not in $\psi_i$ for all $i \in \{1,...,k-1\}$ and not in $\phi$.
$\phi[\psi_1,...,\psi_k/p_1,...,p_k] = \left(\left(\phi[p^'_k/p_k]\right)[\psi_1,...,\psi_{k-1}]\right)[p_k/p^'_k]$