(certify-book "consider-hint-tests" 0 t :skip-proofs-okp t)