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