proposition: Lemma eqs_mapE : forall E l l', eqs l l' -> eqs (map (fun x => Conc x E) l) (map (fun x => Conc x E) l' ).
proof: Proof. move => E l l'; move/eqs_elim => h. apply/eqs_elim => x. split. - case/map_InA => y h1 h2. rewrite (InA_eq sim_dec _ h1). apply: InA_map => //. + by move => a b hs; apply similar_congr_Conc; last reflexivity. by apply h. - case/map_InA => y h1 h2. rewrite (InA_eq sim_dec _ h1). apply: InA_map => //. + by move => a b hs; apply similar_congr_Conc; last reflexivity. by apply 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)