I would like to split a list into two pieces of equal or nearly equal length.

I tried this but I get an error with the function splitTwo:

```
{-@ halfIndex :: i : [a] -> {j : Int | j == div (len i) 2} @-}
halfIndex :: [a] -> Int
halfIndex [] = 0
halfIndex x = div (length x) 2
{-@ splitTwo :: j : [a] -> {i : ([a], [a]) | (len (fst i)) + (len (snd i)) == len j} @-}
splitTwo :: [a] -> ([a], [a])
splitTwo a = splitAt (halfIndex a) a
```

I am only verifying that the length of the two pieces adds up to the length of the entire list.

What other verifications do you think I should do?

Maybe that the list starts with the first piece and ends with the second? And then that the union of the sublists gives the original list? And that the difference in length of the sublists is not too large? And that the length of each sublist does not differ too much from half the length of the original list?