proposition: Lemma in_CAll2: forall u, (u \in CStar CDot).
proof: Proof. elim => [ |hd tl iH] //=. move/starP : iH => [s h1 h2]. apply/starP. exists (cat [:: [::hd]] (map (fun xx => [::xx]) tl)) => //=. apply/allP => x hx. move/mapP : hx => [y hin hy]. by rewrite hy. by rewrite flatten_map_cons. 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)