fact: Definition bregexp_eq (r1 r2: bregexp) : bool := (all delta2 (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)