proposition: Lemma lreg_incl_eqs : forall l1 l2, eqs l1 l2 -> (lreg_incl l1 l2 && lreg_incl l2 l1).
proof: Proof. move => l1 l2. move/eqs_elim => h. apply/andP; split. - apply/lreg_inclP => x hx. case: (@InA_inv _ _ _ sim_dec l2 x _) => [ | y h1 h2]. + apply h. clear h. elim : l1 hx => [ | hd tl hi] //=. rewrite in_cons. case/orP => hu. * case: (sim_dec x hd) => //=. rewrite (eqP hu). case; reflexivity. rewrite (hi hu); by case: (sim_dec x hd). exists y => //. rewrite /reg_incl. transitivity (Plus y y) => //. by symmetry; apply similar_congr_Plus; last reflexivity. - apply/lreg_inclP => x hx. case: (@InA_inv _ _ _ sim_dec l1 x _) => [ | y h1 h2]. + apply h. clear h. elim : l2 hx => [ | hd tl hi] //=. rewrite in_cons. case/orP => hu. * case: (sim_dec x hd) => //=. rewrite (eqP hu). case; reflexivity. rewrite (hi hu); by case: (sim_dec x hd). exists y => //. rewrite /reg_incl. transitivity (Plus y y) => //. by symmetry; apply similar_congr_Plus; last reflexivity. 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)