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