Generic recognizer for the output list type of a projection.
Function:
(defun outelement-list-p (x) (if (atom x) (outelement-list-final-cdr-p x) (and (outelement-p (car x)) (outelement-list-p (cdr x)))))
Theorem:
(defthm outelement-list-p-of-append (implies (and (outelement-list-p x) (outelement-list-p y)) (outelement-list-p (append x y))))