fact: Fixpoint extract_word (l: seq (bregexp*bregexp*bword)) : option bword := match l with | [::] => None | ((a,b),u) :: tl => if has_eps a == has_eps b then extract_word tl else Some u end.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)