fact: Definition mkStar r := match r with | CEps => CEps | CVoid => CEps | CStar _ => r | _ => CStar r end.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)