(acl2::value :q)
(acl2::lp)
(ld '((ubt! 1)
      (ld "define-u-package.lisp")
      (certify-book "defalist" 1)))