proposition: Theorem fst_split_map_eq : forall (A B C : Type)(ls : list A)(f : A -> B * C), fst (split (map f ls)) = map (fun a => fst (f a)) ls.
proof: Proof. induction ls; intuition; simpl in *. remember (f a) as z. destruct z. remember (split (map f ls)) as y. destruct y. simpl. f_equal. assert (l = fst (split (map f ls))). rewrite <- Heqy. trivial. subst. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation