proposition: Lemma flatten_Permutation : forall (A : Type)(ls1 ls2 : list (list A)), Permutation ls1 ls2 -> Permutation (flatten ls1) (flatten ls2).
proof: Proof. induction 1; intuition; simpl in *. eapply Permutation_app. eapply Permutation_refl. trivial. repeat rewrite app_assoc. eapply Permutation_app. eapply Permutation_app_comm. eapply Permutation_refl. eapply perm_trans. eapply IHPermutation1. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia