proposition: Theorem fst_split_app_eq : forall (A B : Type)(ls1 ls2 : list (A * B)), fst (split (ls1 ++ ls2)) = fst (split ls1) ++ fst (split ls2).
proof: Proof. induction ls1; intuition; simpl in *. specialize (IHls1 ls2). remember (split (ls1 ++ ls2)) as z. destruct z. remember (split ls1) as y. destruct y. simpl in *. subst. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation