Lemmas about reverse available in the std/lists library.
The built-in reverse function is overly complex because it can operate on either lists or strings. To reverse a list, it is generally preferable to use rev, which has a very simple definition.
We ordinarily expect
Because of this, we do not expect these lemmas to be very useful unless, for
some reason, you have disabled
(defthm stringp-of-reverse (equal (stringp (reverse x)) (stringp x)))
(defthm true-listp-of-reverse (equal (true-listp (reverse x)) (not (stringp x))))
(defthm equal-of-reverses (equal (equal (reverse x) (reverse y)) (if (or (stringp x) (stringp y)) (and (stringp x) (stringp y) (equal x y)) (equal (list-fix x) (list-fix y)))))