(in-package "ACL2-USER")

(defmacro seq (stobj &rest rst)
(cond ((endp rst) stobj)
      ((endp (cdr rst)) (car rst))
      (t `(let ((,stobj ,(car rst)))
              (seq ,stobj ,@(cdr rst))))))