I would like to note that the chapter "Another Look At Automated Theorem-proving II" seems quite ill informed, and very hostile, to me. For instance, to my kno

I would like to note that the chapter "Another Look At Automated Theorem-proving II" seems quite ill informed, and very hostile, to me. For instance, to my knowledge the Hashed El Gamal proof in Easycrypt checkes the whole proof, not just the hops. (If I understood Remark 2 correctly)