proposition: Lemma Bar_gpred_list : forall E, E_compat E -> IFinite eqA E -> IFinite eql (gpred_list E).
proof: Proof. move => E hE hfE. apply: nS_is_enough ; first done. apply: (@Bar_grel_incl _ _ (r_union (r_inter nS (r_not nR)) nR)). apply: Bar_grel_union. by apply: lemma6. by apply: Bar_gpred_grel. by apply :tool_converse. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)