A character set for
Function:
(defun letter/uscore/dollar-chars$inline nil (declare (xargs :guard t)) 10633823849912963253511222563025453056)
Theorem:
(defthm charset-p-of-letter/uscore/dollar-chars (charset-p (letter/uscore/dollar-chars)))
Theorem:
(defthm char-in-charset-p-of-letter/uscore/dollar-chars (equal (char-in-charset-p x (letter/uscore/dollar-chars)) (letter/uscore/dollar-char-p x)))