proposition: Lemma InA_map : forall (x:regexp) f, (forall x y, similar x y -> similar (f x) (f y)) -> forall l, InA sim_dec l x -> InA sim_dec (map f l) (f x).
proof: Proof. move => x f hf. elim => [ | hd tl hi] => //=. case: (sim_dec x hd) => hsim //=. - move => _; case: sim_dec => //=. case. by apply: hf. move => h; rewrite (hi h). 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)