Some theorems about the built-in function take.
The theorem take-of-1+-to-rcons is disabled by default. It may be useful when reasoning about take and rcons.
Theorem: take-of-1+-to-rcons
(defthm take-of-1+-to-rcons (implies (natp n) (equal (take (1+ n) x) (rcons (nth n x) (take n x)))))
