Gao, Feng, and George Tourlakis. “A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics”. Bulletin of the Section of Logic, vol. 44, no. 3/4, Jan. 2015, pp. 131–147, https://doi.org/10.18778/0138-0680.44.3.4.03.