proposition: Lemma has_eps_sim : forall r1 r2, similar r1 r2 -> has_eps r1 = has_eps r2.
proof: Proof. move => r1 r2. move/similar_ok => h. rewrite !has_epsE. by rewrite (h [::]). 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)