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