(true-p x) recognizes only the symbol t.
Function: true-p
(defun true-p (x) (declare (xargs :guard t)) (eq x t))
