proposition: Lemma flat_map_flatten : forall {A B: Type}, forall comp seq, @flat_map A B comp seq = flatten (map comp seq).
proof: Proof. intros; induction seq; simpl; try rewrite IHseq; reflexivity. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith