proposition: Lemma wder_cat : forall s t E, wder (s++t) E = wder t (wder s E).
proof: Proof. elim => [ | hd tl hi] t E //=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)