proposition: Lemma flatten_app : forall (A : Set)(ls1 ls2 : list (list A)), flatten (ls1 ++ ls2) = flatten ls1 ++ flatten ls2.
proof: Proof. induction ls1; intuition; simpl in *. rewrite <- app_assoc. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation