proposition: Lemma Bar_gpred_grel : forall (R:grel A) (E:gset A), Bar R E -> Bar (grel_list R) (gpred_list E).
proof: Proof. move => R e. elim => [E hp hi]; clear e. apply cBar => xs hxs. apply: (@Bar_gset_incl _ (Finite_Union (tool_list_to_prodn E R xs))). apply: Finite_Union_is_finite. elim : xs hxs => [ | hd tl Ihxs] /=; first done. case => hhd htl. split. by apply: hi. by apply: Ihxs. clear hp hi. move => y [hy ]. elim : xs hxs => [ | hd tl hi] //=. case => hhd htl [ | ]. move => hy2. left. by apply: gpred_list_inter. move => hrel; right. 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)