proposition: Theorem snd_split_app : forall (A B : Type)(ls1 ls2 : list (A * B)), snd (split (ls1 ++ ls2)) = (snd (split ls1)) ++ (snd (split ls2)).
proof: Proof. induction ls1; intuition idtac; simpl in *. remember (split (ls1 ++ ls2)) as z. destruct z. simpl. remember (split ls1) as z'. destruct z'. simpl. f_equal. simpl in *. assert (l0 = snd (split (ls1 ++ ls2))). rewrite <- Heqz. trivial. subst. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation