Some theorems about the library function rev.
The theorems car-of-rev-rewrite-car-of-last
are disabled by default.
They may be useful to turn (car (rev ...)) into (car (last ...))
or vice versa.
A theory invariants prevents them from being both enabled
(which would cause a loop in the rewriter).
Definitions and Theorems
(equal (car (rev x)) (car (last x))))
(equal (car (last x)) (car (rev x))))