Rev-theorems
Some theorems about the library function rev.
The theorems car-of-rev-rewrite-car-of-last
and car-of-last-rewrite-car-of-rev
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
Theorem: car-of-rev-rewrite-car-of-last
(defthm car-of-rev-rewrite-car-of-last
(equal (car (rev x)) (car (last x))))
Theorem: car-of-last-rewrite-car-of-rev
(defthm car-of-last-rewrite-car-of-rev
(equal (car (last x)) (car (rev x))))
