proposition: Lemma set_of_der_compat : forall E x y, sim x y -> set_of_der E x -> set_of_der E y.
proof: Proof. rewrite /set_of_der => E x y. rewrite /sim => heq. case => s heq2. exists s. transitivity x => //. by symmetry. 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)