On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic