proposition: Theorem unzip_eq_split : forall (A B : Set)(ls : list (A * B)), unzip ls = split ls.
proof: Proof. induction ls; intuition; simpl in *. remember (split ls) as z. destruct z. unfold unzip. simpl. f_equal. f_equal. assert (l = fst (l, l0)). trivial. rewrite H. rewrite <- IHls. trivial. assert (l0 = snd (l, l0)). trivial. rewrite H. rewrite <- IHls. f_equal. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation