proposition: Lemma incl_der_pred_star : forall E, Included (set_of_der (Star E)) (Union (pred_singl (Star E)) (set_of_der_star E )).
proof: Proof. move => E F. case => [] s /=. move: (wder_Star s E). case : s => [ | hd tl]. - move => h1 heq. left. rewrite /pred_singl. by transitivity (wder [::] (Star E)). move => h1 heq; right. apply : (@incl_star_tool tl hd E F [::]). by transitivity (wder (hd :: tl) (Star E)). 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)