proposition: Lemma incl_der_pred_and: forall E F, Included (set_of_der (And E F)) (pred_and (set_of_der E) (set_of_der F)).
proof: Proof. move => E F x. rewrite /In /set_of_der. case => u. rewrite wder_And. move=> h2. exists (wder u E); exists (wder u F); split. by exists u; reflexivity. split => //. by exists u; reflexivity. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)