proposition: Lemma incl_der_pred_plus: forall E F, Included (set_of_der (Plus E F)) (pred_plus (set_of_der E) (set_of_der F)).
proof: Proof. move => E F x. rewrite /In /set_of_der. case => u. rewrite wder_Plus. move=> h2. rewrite /pred_plus. - exists (wder u E); exists (wder u F); split. 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)