proposition: Lemma wder_sigma_switch : forall t s x E F, wder_sigma (der x E) F s t = wder_sigma E F [:: x & s] t.
proof: Proof. elim => [ | hd tl hi] s x E F //=. case (has_eps (wder s (der x E))). congr Plus. by rewrite hi. by rewrite hi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)