fact: Fixpoint DER l := match l with | [::] => [::] | ((hdl,hdr),s) :: tl => [:: (der1 hdl, der1 hdr, true::s) , (der0 hdl, der0 hdr, false::s) & DER tl ] end.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)