proposition: Lemma gpred_list_DERs : forall E F, (forall X, gpred_list (Prod (set_pair_ders E F) bT) X -> gpred_list (Prod (set_pair_ders E F) bT) (DER X)).
proof: Proof. move => E F. elim => [ | [[hdl hdr] u] tl] //= => hi. case => [[[s -> ->] _]] htl; split. by split => //; exists (s++[::true]); rewrite /der1 !wder_cat /=. split. by split => //; exists (s++[::false]); rewrite /der0 !wder_cat /=. by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)