proposition: Lemma reg_incl_has : forall x l, has (reg_incl x) l -> forall r, reg_incl x (rPlus r l).
proof: Proof. move => x. elim => [ | hd tl hi] //=. case/orP => hu r. - by apply reg_incl_Pr. by apply reg_incl_Pl; apply: hi. 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)