Lemmas for reducing list-equiv terms involving basic functions.
Theorem:
(defthm list-equiv-of-cons-and-cons (equal (list-equiv (cons a x) (cons a y)) (list-equiv x y)))
Theorem:
(defthm list-equiv-of-append-and-append (equal (list-equiv (append a x) (append a y)) (list-equiv x y)))
Theorem:
(defthm list-equiv-of-revappend-and-revappend (equal (list-equiv (revappend a x) (revappend a y)) (list-equiv x y)))