proposition: Lemma wder_Conc: forall u E F, wder u (Conc E F) = wder_sigma E F [::] u.
proof: Proof. elim => [ | hd tl hi] E F //=. case: (has_eps E). - by rewrite wder_Plus hi wder_sigma_switch. by rewrite hi wder_sigma_switch. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)