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