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