(in-package "ACL2")

(defun remove-nth (i x)
  (declare (xargs :guard (and (natp i)
                              (true-listp x))))
  (cond ((endp x) nil)
        ((zp i) (cdr x))
        (t
         (cons (car x)
               (remove-nth (1- i) (cdr x))))))

(defthm len-remove-nth
  (implies (and (consp x)
                (< i (len x)))
           (equal (len (remove-nth i x))
                  (- (len x) 1))))

(defthm true-listp-remove-nth
   (implies (true-listp x)
            (true-listp (remove-nth i x))))