proposition: Theorem fst_split_flatten_eq : forall (A B : Type)(ls : list (list (A * B))), fst (split (flatten ls)) = flatten (map (fun x => fst (split x)) ls).
proof: Proof. induction ls; intuition; simpl in *. rewrite fst_split_app_eq . f_equal. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation