Lemmas about reverse available in the std/lists
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 reverse to be enabled, in which case it
expands (in the list case) to (revappend x nil), which we generally expect
to be rewritten to (rev x) due to the revappend-removal theorem.
Because of this, we do not expect these lemmas to be very useful unless, for
some reason, you have disabled reverse itself.
Definitions and Theorems
(equal (stringp (reverse x))
(equal (true-listp (reverse x))
(not (stringp x))))
(equal (equal (reverse x) (reverse y))
(if (or (stringp x) (stringp y))
(and (stringp x)
(equal x y))
(equal (list-fix x) (list-fix y)))))