proposition: Lemma CPlus_cons : forall hd tl u, (u \in CPlus (hd :: tl) )= (u \in hd ) || (u \in CPlus tl).
proof: Proof. move => hd tl u. rewrite -!topredE /= /mem_creg /=. by apply/orP/orP. 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)