This is an ordinary defenum.
Function:
(defun wiretype (x) (declare (xargs :guard t)) (or (eq x 'nil) (eq x ':supply0) (eq x ':supply1) (eq x ':wand) (eq x ':wor) (eq x ':tri0) (eq x ':tri1) (eq x ':trireg)))
Theorem: type-when-wiretype
(defthm type-when-wiretype (implies (wiretype x) (if (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil) 't (equal x 'nil))) :rule-classes :compound-recognizer)