(certify-book "macros-skip-proofs" 0 t :skip-proofs-okp t)