Recognizer for specqual structures.
(specqualp x) → *
Theorem: consp-when-specqualp
(defthm consp-when-specqualp (implies (specqualp x) (consp x)) :rule-classes :compound-recognizer)