proposition: Lemma flatten_nils : forall {A} (seq: list (list A)), flatten (List.map (fun _ => []) seq) = @nil A.
proof: Proof. induction seq; intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith