proposition: Lemma lreg_inclP : forall l1 l2, reflect (forall x, (x \in l1) -> exists2 y, (y \in l2) & reg_incl x y) (lreg_incl l1 l2).
proof: Proof. rewrite /lreg_incl => l1 l2. apply: (iffP idP). - move/allP => ha x hx. by move/hasP : (ha x hx). move => h. apply/allP => x hx. apply/hasP. by apply: h. 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)