proposition: Lemma rPlus2_congr : forall l c1 c2 e1 e2, similar c1 c2 -> similar e1 e2 -> similar (rPlus2 c1 e1 l) (rPlus2 c2 e2 l).
proof: Proof. rewrite /rPlus2 => l c1 c2 e1 e2 h1 h2. elim: l => [ | hd tl hi] //=. apply similar_congr_Plus. - by apply hi. by apply similar_congr_Conc; [reflexivity | done ]. 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)