proposition: Theorem Permutation_flatten : forall (A : Set)(ls1 ls2 : list (list A)), Permutation ls1 ls2 -> Permutation (flatten ls1) (flatten ls2).
proof: Proof. induction 1; intuition; simpl in *. eapply Permutation_app_head. trivial. repeat rewrite app_assoc. eapply Permutation_app_tail. eapply Permutation_app_comm. eapply Permutation_trans; eauto. Qed.
imports: FCF.FCF Permutation