proposition: Lemma mem_derE : forall u e, mem_der e u = (u \in e).
proof: Proof. by elim=> [|x u IHu] e /=; rewrite ?has_epsE // IHu derE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)