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