fact: Fixpoint mem_der e u := if u is x :: v then mem_der (der x e) v else has_eps e.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)