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