proposition: Lemma CPlus_cat : forall l1 l2 u, (u \in CPlus (l1++l2)) = (u\in CPlus l1) || (u \in CPlus l2).
proof: Proof. elim => [ | hd tl hi] l2 //= u. by rewrite !CPlus_cons (hi l2) orbA. 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)