proposition: Lemma DER_preserves_lang : forall E F X, gpred_list (ff E F) X -> gpred_list (ff E F) (DER X).
proof: Proof. move => E F. elim => [ | [[r1 r2] u] tl hi] //= [[h1 h2] h3]. rewrite !rev_cons !wder_rcons /=. split. - split. move => s. by apply in_der_compat. - move => s; by apply in_der_compat. - split. split. move => s; by apply in_der_compat. - move => s; by apply in_der_compat. 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)