proposition: Lemma mkConc_unfold2: forall l r, [/\ r != CVoid, r != CEps & (forall l, r != CConc l) ] -> mkConc r (CConc l) = CConc (r::l).
proof: Proof. move => l. case => [ | | | s | c | l' | l' | l' | c ] //=. - by case. - by case. - case => _ _ h. move/negP: (h l'). by case. 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)