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))

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.