proposition: Lemma length_flatten_eq : forall (A B : Set)(lsa : list (list A))(lsb : list (list B)), list_pred (fun a1 a2 => length a1 = length a2) lsa lsb -> length (flatten lsa) = length (flatten lsb).
proof: Proof. induction 1; intuition; simpl in *. repeat rewrite app_length. f_equal. trivial. trivial. Qed.
imports: FCF.FCF Permutation