(certify-book "exercise1" 0 t :defaxioms-okp t)