[ new ] Interleaving of Lists

[gallais]

This has been sitting on a branch for a while. Might as well start a PR.

[MatthewDaggitt]

Looks good! My only comment is that maybe Split is a bit confusing as a name as when you split something you typically only use a single break. Interleave would be much clearer. Would you object to me changing it?

[gallais]

As I said in the first commit message:

I have changed my mind and called it Split because the List being broken down
is the first argument of the relation.

I am a bit uneasy because Interleave xs ys zs intuitively suggests to me that I get
zs by interleaving xs and ys rather than the other way around. That being said, it
is not that big of a deal to me so I won't oppose a name change.

[MatthewDaggitt]

I am a bit uneasy because Interleave xs ys zs intuitively suggests to me that I get
zs by interleaving xs and ys rather than the other way around.

What about if we changed the definition to match that intuition?

[gallais]

That could work. We would presumably need to flip the relations too to keep the
arguments in the same order as the indices'.

[MatthewDaggitt]

I'll give it a go at some point and see what it reads like.

[MatthewDaggitt]

I've updated the name to Interleaving and swapped the argument order. I've also thrown in Propositional interleavings for the sake of it, and move toPermutation there.