proposition: Lemma flatten_app : forall {A} (seq1 seq2: list (list A)), flatten (seq1 ++ seq2) = flatten seq1 ++ flatten seq2.
proof: Proof. unfold flatten; induction seq1; simpl; trivial. intros; rewrite IHseq1; rewrite app_assoc; trivial. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith