proposition: Lemma flatten_map_cons : forall (A:Type) (l:seq A), flatten (map (fun xx => [::xx]) l) = l.
proof: Proof. move => A; elim => [ | hd tl ih] //=. by rewrite {1}ih. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)