proposition: Lemma gpred_listP2 : forall (A:eqType) (E:gset A) (l:seq A) (x:A), (x \in l) -> gpred_list E l -> E x.
proof: Proof. move => A E l x. elim: l => [ | hd tl hi] //=. rewrite in_cons. case/orP => hu [hhd htl]. by rewrite (eqP hu). by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)