Std/basic/member-symbol-name
Theorems about the built-in function member-symbol-name.
Definitions and Theorems
Theorem: member-symbol-name-when-atom
(defthm member-symbol-name-when-atom
(implies (atom symbols)
(not (member-symbol-name string symbols))))
