Rewrite (take n x) when n is more than (len x).
This rule may sometimes lead your proof in a bad direction. If you
see unwanted repeat terms, you may want to disable it.
Definitions and Theorems
(implies (<= (len x) (nfix n))
(equal (take n x)
(append x (repeat (- (nfix n) (len x)) nil)))))