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