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