(in-package "ACL2")
(include-book "book3b")
(defun g (x) x)