proposition: Lemma EF_in_der : forall (E F:bregexp), gpred_list (Prod (set_pair_ders E F) bT) [:: (E,F,[::])].
proof: Proof. rewrite /set_pair_ders /= => E F. split => //. by split; [exists [::] | ]. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)