fact: Definition bregexp_ce (r1 r2:bregexp) : option bword := extract_word (build_list_fun r1 r2).
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)