proposition: Lemma CAnd_cat : forall l1 l2 u, (u \in CAnd (l1++l2)) = (u\in CAnd l1) && (u \in CAnd l2).
proof: Proof. elim => [|hd tl hi] l2 //= u. by rewrite !CAnd_cons (hi l2) andbA. 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)