I want to define a lambda term $\mathrm{swapQ}$ such that
$$\begin{align} \mathrm{swapQ}\ &(\lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \triangleright_\beta\ & (\lambda P Q_1 Q_2. Q_2 (\lambda x_2. Q_1(\lambda x_1. Px_1 x_2))) \end{align}$$
So far I have come up with $$\mathrm{swapQ^*} := \lambda S' P' Q_1' Q_2'. S' P' Q_2' Q_1' \\ \begin{align} \mathrm{swapQ^*}\ &(\lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \triangleright_\beta\ & (\lambda P Q_1 Q_2. Q_2 (\lambda x_1. Q_1(\lambda x_2. Px_1 x_2))) \end{align}$$
but this only swaps the $Q_i$s, not the $\lambda x_i$s that should go with them.
After having fiddled around for a while, I can not seem to find a way to change order of the variable abstractions while leaving the variable occurrences inside the term intact (or vice versa for an equivalent expression). I probably need to abstract over the $(\lambda x_i. \ldots$) parts and reapply them in the same way I did with the $Q$'s, but I can not find the right way to "inject" this override application at the right place without taking the embedded applications with them.
Is what I want to do possible at all? I would appreciate hints for the right technique or perhaps pointers to the literature in case this has been done before.
Background:
In Montague grammar for formal natural language semantics, sentences can be formed by consecutively applying $n$ quantified expressions $Q_i$ (where quantified expressions are functions from sets of individuals to truth values) to an $n$-ary verb $P$ (where an $n$-ary verb is a function from $n$ individuals to truth values) to produce a statement. For instance,
$$ \begin{align} & \mathrm{(sentence)(loves)((every)(woman))((a)(man))}\\ \triangleright_\beta & (\mathrm{(every\ woman)}(\lambda x_1. (\mathrm{(a\ man)}(\lambda x_2. \mathrm{loves}x_1x_2))))\\ \triangleright_\beta & \forall x (Wx \to \exists y (My \land Lxy))\\ & \text{"Every woman loves a man"} \end{align} $$ where $$\begin{align} \mathrm{sentence} = & \lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \mathrm{every} = & \lambda P_1 P_2. \forall x (P_1x \to P_2x)\\ \mathrm{a} = & \lambda P_1 P_2. \exists x (P_1x \land P_2x)\\ \mathrm{loves} = & \lambda x y. Lxy\\ \mathrm{woman} = & \lambda x. Wx\\ \mathrm{man} = & \lambda x. Mx\\ \end{align}$$ and application is left-associative ($MNP = (MN)P$).
The purpose of the $\mathrm{swapQ}$ combinator is to swap the two quantified expressions to produce the inverted scope reading, such that
$$\begin{align} & \mathrm{((swapQ)(sentence))(loves)((every)(woman))((a)(man))}\\ \triangleright_\beta & (\mathrm{(a\ man)}(\lambda x_2. (\mathrm{(every\ woman)}(\lambda x_1. \mathrm{loves}x_1x_2))))\\ \triangleright_\beta & \exists y (My \land \forall (Wx \to Lxy))\\ & \text{"There is a man every woman loves"} \end{align}$$ That is, the swapping combinator is applied to the sentence forming combinator such that the order in which the quantified expressions take scope over each other is swapped, while retaining their associated argument position in the verb (determined by which $x_i$ the quantifiers bind to) such that subject remains subject and object remains object.
The motivation is linguistic, but the problem is a purely lambda-technical one, so I figured it is best off at MathSE.
