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