How the language $\{a^nb^mc^nd^m | n \geq1, \ m\geq1\}$ is used to check whether formal and actual parameters are equal?
The language

$$L=\{a^nb^mc^nd^m \mid n \geq1, m\geq1\}$$

abstracts agreement of parameter and argument count for the case where there are exactly two procedures, one with $n$ parameters, declared with $a^n$ and used with $c^n$, and the other one with $m$ parameters, declared with $b^m$ and used with $d^m$. Each procedure is called exactly once and the calls are interleaved with the declarations. The interleaving makes it impossible for a context-free grammar to specify agreement.

One might be tempted to generalize to more uses of each procedure:

$$L'=\{a^nb^m\omega \mid n \geq1, m\geq1, \omega \in \{c^n,d^m\}^*\}$$

or more procedures (I'm not going to try writing that one out), but it just serves to make everything more complicated to no purpose.

The simple example is easily proven to not be context free, and the simplification can be justified by observing that context-free languages are closed under substitution which is a very powerful and useful proof technique. (The fact that declarations and uses can be reduced to repetition of a simple symbol is also justified by substitution. A starting point for Algol-style languages might be to remove all the parameters/arguments from a declaration/call, leaving only the commas and parentheses. For S-expressions it's even simpler.)

So the abstraction provides a simple proof (as well as some intuitive basis) for why parameter/argument agreement cannot be incorporated into a context-free grammar.