Gao, F.; Tourlakis, G. A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics. B Sect Log 2015, 44, 131–147.