(include-book "eval")

(certify-book "embedded-defaxioms" 1 t :ttags (:writes-okp))