proposition: Lemma fStar_compat : forall a a' : regexp * regexp * seq regexp, eqtemp a a' -> similar (fStar a) (fStar a').
proof: Proof. case => [[e f] l] [[e' f'] l']. rewrite /eqtemp /eq_prod /fStar /rPlus2. rewrite /sim => /= [[[he1 he2]]]. move/(eqs_mapE (Star f)). move/lreg_incl_eqs. case/andP. move/lreg_incl_reg => h1. move/lreg_incl_reg => h2. transitivity (rPlus (Conc e (Star f)) (map (fun x => Conc x (Star f)) l')). - by rewrite -reg_incl_sim (h1 (Conc e (Star f))) (h2 (Conc e (Star f))). apply rPlus2_congr. - apply similar_congr_Conc => //. by apply similar_congr_Star. by apply similar_congr_Star. 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)