# Splitting and combining lists

Define two functions with the foolowing type
`
split
: forall A B : Set, list (A * B) -> list A * list B
combine
: forall A B : Set, list A -> list B -> list (A * B)
`
and the usual behavior (transform a list of pairs into
a pair of lists containing the same data, and vice-versa, whenever possible)

Prove a simple theorem relating `split` and `combine`
## Solution

Look at this file

Going home

Pierre Castéran