proposition: Lemma incl_der_pred_conc : forall E F, Included (set_of_der (Conc E F)) (set_of_der_conc E F).
proof: Proof. move => E F G. case => s. rewrite wder_Conc. elim: s E F G => [ | hd tl hi] E F G /=. - move => h. exists E, [::] => /= ; split. + by exists [::]; reflexivity. by split. case : (has_eps E). - rewrite -wder_sigma_switch. case: (@hi (der hd E) F (wder_sigma (der hd E) F [::] tl)). + reflexivity. move => G' [l ]. case => [[s hs] [h1 h2]] hG. exists (wder (hd::s) E). exists (cons (wder (hd :: tl) F) l); split. + exists (hd :: s); by reflexivity. split => /=. + split => //. exists (hd::tl); by reflexivity. transitivity (Plus (wder_sigma (der hd E) F [::] tl) (wder tl (der hd F))) => //. apply similar_congr_Plus; last reflexivity. transitivity (rPlus (Conc G' F) l) => //. apply rPlus_congr. apply similar_congr_Conc; [ done | reflexivity]. rewrite -wder_sigma_switch. case: (@hi (der hd E) F (wder_sigma (der hd E) F [::] tl)). - reflexivity. move => G' [l]. case => [[s hs] [h1 h2]] hG. exists (wder (hd :: s) E). exists l; split. - exists (hd :: s); reflexivity. split => //=. transitivity (wder_sigma (der hd E) F [::] tl) => //. transitivity (rPlus (Conc G' F) l) => //. apply rPlus_congr. apply similar_congr_Conc ; [ done | 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)