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