proposition: Lemma length_flatten : forall (A : Set)(ls : list (list A)), length (flatten ls) = fold_left (fun acc a => (acc + (length a))%nat) ls O.
proof: Proof. induction ls; intuition; simpl in *. rewrite app_length. rewrite fold_add_init_nat. f_equal. eauto. Qed.
imports: FCF.FCF Permutation