fact: Definition EQUIV (E F:bregexp) := forall s:bword, (s \in E ) = (s \in F).
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)