Lemmas about subseq-list available in the std/lists library.

ACL2's built-in

**Function: **

(defun subseq-list (lst start end) (declare (xargs :guard (and (true-listp lst) (integerp start) (integerp end) (<= 0 start) (<= start end)))) (take (- end start) (nthcdr start lst)))

Unfortunately

It is often pretty reasonable to just leave

**Theorem: **

(defthm len-of-subseq-list (equal (len (subseq-list x start end)) (nfix (- end start))))

**Theorem: **

(defthm consp-of-subseq-list (equal (consp (subseq-list x start end)) (posp (- end start))))

**Theorem: **

(defthm subseq-list-under-iff (iff (subseq-list x start end) (posp (- end start))))

**Theorem: **

(defthm subseq-list-of-list-fix (equal (subseq-list (list-fix x) start end) (subseq-list x start end)))

**Theorem: **

(defthm list-equiv-implies-equal-subseq-list-1 (implies (list-equiv x x-equiv) (equal (subseq-list x start end) (subseq-list x-equiv start end))) :rule-classes (:congruence))

**Theorem: **

(defthm subseq-list-starting-from-zero (equal (subseq-list x 0 n) (take n x)))

**Theorem: **

(defthm subseq-list-of-len (implies (natp n) (equal (subseq-list x n (len x)) (nthcdr n (list-fix x)))))