(include-book "eval")

(certify-book "assert-check-include-1" 1 t :save-expansion t)