Included Books
other
(in-package "ACL2")
include-book
(include-book "lookup-eq-def")
include-book
(include-book "lookup-equal-def")
lookup-eq-becomes-lookup-equaltheorem
(defthm lookup-eq-becomes-lookup-equal (equal (lookup-eq key alist) (lookup-equal key alist)) :hints (("Goal" :in-theory (enable lookup-equal lookup-eq))))