Generic recognizer for the output element type of a projection.
Theorem: outelement-p-of-outelement-example
(defthm outelement-p-of-outelement-example (outelement-p (outelement-example)))