proposition: Lemma gpred_list_incl : forall (E F:gset A), (forall (x:A), F x -> E x) -> forall (l:seq A), gpred_list F l -> gpred_list E l.
proof: Proof. move => E F h. elim => [ | hd tl hi] //= [hin hpred]. split. by apply: h. by apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)