equal-of-booleans - ACL2 Book

other

(in-package "ACL2")

equal-of-booleans-cheaptheorem

(defthm equal-of-booleans-cheap
  (implies (and (booleanp x) (booleanp y))
    (equal (equal x y) (iff x y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

equal-of-booleanstheorem

(defthmd equal-of-booleans
  (implies (and (booleanp x) (booleanp y))
    (equal (equal x y) (iff x y))))