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