Simplify and add some internal documentation to the compilation of coinduction hook predicates