Flatten a pattern into a list of atoms (with an accumulator).
(pat-flatten pat acc) flattens
(pat-flatten '((a) (b c)) '(x y z)) --> (a b c x y z)
The accumulator argument is occasionally useful. But for reasoning, we
(defthm pat-flatten-is-pat-flatten1 (equal (pat-flatten pat acc) (append (pat-flatten1 pat) acc)))