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