(in-package "ACL2")
(include-book "must-be-redundant")
(include-book "must-succeed-star")
(must-succeed* (defun f (x) x) (must-be-redundant (defun f (x) x)) (defthm th (acl2-numberp (+ x y))) (must-be-redundant (defthm th (acl2-numberp (+ x y)))))