Rewrite rule that eliminates make-list-ac (and hence make-list) in favor of repeat.
Theorem: make-list-ac-removal
(defthm make-list-ac-removal (equal (make-list-ac n x acc) (append (repeat n x) acc)))