proposition: Lemma wder_Star : forall u E, similar (wder u (Star E)) (match u with | [::] => Star E | _ => wder_sigma E (Star E) [::] u end).
proof: Proof. elim => [ | hd tl hi] E //=. - reflexivity. rewrite wder_Conc wder_sigma_switch. case: (has_eps E). - by symmetry. 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)