proposition: Lemma map_InA : forall (x:regexp) f l, InA sim_dec (map f l) x -> exists2 y, similar x (f y) & InA sim_dec l y.
proof: Proof. move => x f; elim => [ | hd tl hi] //=. case: (sim_dec x (f hd)) => //=. - rewrite /sim => h _; exists hd => //. case: sim_dec => //=. case; reflexivity. move => _ h; case : (hi h) => y h1 h2. exists y => //. rewrite h2; by case: sim_dec. 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)