Generic typed list valtype recognizer.
Theorem: non-valtype-p-def
(defthm non-valtype-p-def (iff (non-valtype-p x) (not (valtype-p x))))