Some theorems about the list primitive functions (i.e. car, cdr, cons, and consp).
Theorem: list-of-car-when-one
(defthm list-of-car-when-one (implies (and (consp list) (not (consp (cdr list)))) (equal (list (car list)) (true-list-fix list))))
