Recognizer for amb-decl/stmt structures.
(amb-decl/stmt-p x) → *
Theorem: consp-when-amb-decl/stmt-p
(defthm consp-when-amb-decl/stmt-p (implies (amb-decl/stmt-p x) (consp x)) :rule-classes :compound-recognizer)
