(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))))))