proposition: Lemma lreg_incl_reg : forall l1 l2, lreg_incl l1 l2 -> forall r, reg_incl (rPlus r l1) (rPlus r l2).
proof: Proof. elim => [ | hd tl hi] l2 //=. - move => _ r; by apply : lreg_incl1. case/andP => h1 h2 r. apply reg_incl_Plus. rewrite (hi l2 h2 r) /=. by apply reg_incl_has. 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)