proposition: Lemma fConc2_compat : forall a a' : regexp * regexp * seq regexp, eqtemp a a' -> similar (fConc2 a) (fConc2 a').
proof: Proof. case => [[e f] l] [[e' f'] l']. rewrite /eqtemp /eq_prod /fConc2. rewrite /sim /= => [[[he1 he2]]]. move/lreg_incl_eqs. case/andP. move/lreg_incl_reg => h1. move/lreg_incl_reg => h2. transitivity (rPlus (Conc e f) l'). - by rewrite -reg_incl_sim (h1 (Conc e f)) (h2 (Conc e f)). apply rPlus_congr. by apply similar_congr_Conc. 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)