sublis-var-simple

(mutual-recursion (defund sublis-var-simple
    (alist term)
    (declare (xargs :guard (and (symbol-alistp alist) (pseudo-termp term))
        :measure (acl2-count term)))
    (cond ((variablep term) (let ((res (assoc-eq term alist)))
          (if res
            (cdr res)
            term)))
      ((fquotep term) term)
      (t (cons-with-hint (ffn-symb term)
          (sublis-var-simple-lst alist (fargs term))
          term))))
  (defund sublis-var-simple-lst
    (alist terms)
    (declare (xargs :measure (acl2-count terms)
        :guard (and (symbol-alistp alist) (pseudo-term-listp terms))))
    (if (endp terms)
      nil
      (cons-with-hint (sublis-var-simple alist (car terms))
        (sublis-var-simple-lst alist (cdr terms))
        terms))))