# Permutation with firstn and skipn

I’ve been struggling with this part of a proof because of the firstn and skipn part.

Permutation (x :: a :: a0 :: l)
(firstn (length (a :: a0 :: l) / 2) (a :: a0 :: l) ++
x :: skipn (length (a :: a0 :: l) / 2) (a :: a0 :: l))

You can simplify your theorem: the `a :: a0 :: l` is immaterial.

``````Permutation (x :: l0)
(firstn (length l0 / 2) l0 ++
x :: skipn (length l0 / 2) l0)
``````

The specific length is also irrelevant:

``````Permutation (x :: l0) (firstn n l0 ++ x :: skipn n l0)
``````

From there you should be able `Permutation` and `List` lemmas to finish the proof.