Included Books
other
(in-package "ACL2")
local
(local (include-book "../pass1/top"))
rewrite-linear-inequalities-to-ifftheorem
(defthm rewrite-linear-inequalities-to-iff (equal (equal (< w x) (< y z)) (iff (< w x) (< y z))))
in-theory
(in-theory (disable rewrite-linear-inequalities-to-iff))