P. Gerhardy, “The Role of Quantifier Alternations in Cut Elimination”, BRICS, vol. 10, no. 46, Dec. 2003.