proposition: Lemma flatten_map_pair_eq : forall (A B C : Set)(ls : list (list A * list B))(f : A * B -> C), (forall ls1 ls2, In (ls1, ls2) ls -> length ls1 = length ls2) -> flatten (map (fun p => [ls1, ls2] <-2 p; map f (zip ls1 ls2)) ls) = map f (zip (flatten (fst (unzip ls))) (flatten (snd (unzip ls)))).
proof: Proof. induction ls; intuition; simpl in *. rewrite IHls. rewrite <- zip_app. rewrite map_app. trivial. eapply H. intuition. eapply length_flatten_eq. eapply list_pred_map_r'. eapply list_pred_map_l'. eapply list_pred_single. intuition. destruct a. simpl. eapply H. intuition. intuition. Qed.
imports: FCF.FCF Permutation