Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
the checker, and it was not used before that anyway.