proposition: Theorem combine_split_eq : forall (A B : Type)(x : list (A * B)), (combine (fst (split x)) (snd (split x))) = x.
proof: Proof. induction x; intuition idtac; simpl in *. remember (split x) as z. destruct z. simpl in *. subst. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation