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