(in-package "ACL2") (include-book "book4")