Chained substitutions of an application in $\lambda$-calculus, e.g. $AB[C/x][D/y]$ Let $A[C/x]$ denote substitution of $C$ for $x$ in $A$.
Suppose we arrived at the expression $AB[C/x][D/y]$ and we want to manipulate it as follows:
$$
\begin{aligned}
AB[C/x][D/y] &= \Big(\big((AB)[C/x]\big)[D/y]\Big)\\
&= \Big(\big((A[C/x])(B[C/x])\big)[D/y]\Big)\\
&= \Big(\big((A[C/x])[D/y]\big)\big((B[C/x])[D/y]\big)\Big)\\
&= \big(A[C/x][D/y]\big)\big(B[C/x][D/y]\big)\\
\end{aligned}
$$

*

*Can we perform the above manipulations always?

*Or only if certain conditions hold?

*

*such as $x \neq y \text{ and } \big(y \not \in \textsf{FV}(C) \text{ or } x \not \in \textsf{FV}(AB)\big)$ (see below)




Here's one way to arrive at $AB[C/x][D/y]$:
$\beta$-reduction is, of course, defined in terms of substitution as:
$$(\lambda x.A)\ C \rightarrow_{\beta} A[C/x]$$
Under certain conditions, we have
$$(\lambda xy.AB)\ C\ D \twoheadrightarrow_{\beta} AB[C/x][D/y]$$
Proof:
$$
\begin{aligned}
(\lambda xy.AB)\ C\ D &\rightarrow_{\beta} ((\lambda y.AB)[C/x])\ D\\
&\equiv (\lambda y.(AB[C/x]))\ D &&\text{conditions: } x \neq y \text{ and } \big(y \not \in \textsf{FV}(C) \text{ or } x \not \in \textsf{FV}(AB)\big)\\
&\rightarrow_{\beta} (AB[C/x])[D/y]\\
&\equiv AB[C/x][D/y]
\end{aligned}
$$
 A: What you described above sounds nothing but successive substitutions in lambda calculus and we certainly need some rules for it to be manipulated like you specified as referenced here:

Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any lambda expression):


$1. x[x := N] = N \\
2. y[x := N] = y, \text{if}~ x ≠ y \\
3. (M_1 M_2)[x := N] = (M_1[x := N]) (M_2[x := N]) \\
4. (λx.M)[x := N] = λx.M \\
5. (λy.M)[x := N] = λy.(M[x := N]), \text{if}~ x ≠ y ~\text{and}~ y ∉ FV(N) \\
6. \text{To substitute into an abstraction, it is sometimes necessary to α-convert the expression.}$


β-reduction is defined in terms of substitution...

So in your first example if both $A,B$ are terms without abstraction, then you can always have $AB[C/x][D/y]=(A[C/x][D/y])(B[C/x][D/y])$ and further possible result may be based on the specific content of $A,B$. For example, if $A$ doesn't contain variable $x$ and $x \neq y$ then your substitution $[C/x]$ will have no effect on $A$. On the other hand, if your expressions have lambda abstraction(s), then you need to match the conditions of any of the rules 4/5/6 above to proceed accordingly.
Finally successive substitution is different from simultaneous substitution as shown from following example using your notation. If $M ≡ x_1x_2$, then the successive substitution results in $(M[x_1 /x_2])[u/x_1] ≡ [u/x_1 ](x_1x_1) ≡ uu$, while the simultaneous substitution results in $M[x_1 /x_2, u/x_1] ≡ ux_1$.
