F. Gao and G. Tourlakis, “A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics”, B Sect Log, vol. 44, no. 3/4, pp. 131–147, Jan. 2015.