Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. - Christian Urban; Bozhi Zhu (RTA, 2008)