Recognize a pseudo-variable (a symbol or 1).
;; A "pseudo-variable" is either a variable or the constant 1. (defun pseudo-varp (x) (declare (xargs :guard t)) (or (symbolp x) (equal x '1)))
