other
(in-package "ACL2")
not-member-symbol-name-when-not-consptheorem
(defthm not-member-symbol-name-when-not-consp (implies (not (consp l)) (not (member-symbol-name str l))) :hints (("Goal" :in-theory (enable member-symbol-name))))