In turning first/second order formula into Prenex form, it seems that second order quantifiers may fall under the scope of first order quantifiers or vice-versa in the prefix. The matrix is quantifier free.
My question is under what conditions we are allowed to bring second order quantifiers out of the scope of first order quantifiers within the prefix?
The section 3.3 in https://www.logic.at/lvas/185301/Leivant_higher-order-logic.pdf
mentions that transformation, but it is not very clear explanation.