proposition: Lemma incl_der_pred_not : forall E, Included (set_of_der (Not E)) (pred_not (set_of_der E)).
proof: Proof. move => E x. rewrite /set_of_der. case => u. rewrite wder_Not. move=> h2. exists (wder u E); 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)