Check whether an annotated term is a variable.
(atj-type-wrapped-variable-p term) → yes/no
That is, we must first unwrap the term, and then check whether it is a variable.
Function:
(defun atj-type-wrapped-variable-p (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atj-type-wrapped-variable-p)) (declare (ignorable __function__)) (b* (((mv term & &) (atj-type-unwrap-term term))) (variablep term))))
Theorem:
(defthm booleanp-of-atj-type-wrapped-variable-p (b* ((yes/no (atj-type-wrapped-variable-p term))) (booleanp yes/no)) :rule-classes :rewrite)