proposition: Lemma nS_is_enough: forall E, IFinite eqA E -> Bar nS (gpred_list E) -> IFinite eql (gpred_list E).
proof: Proof. rewrite /IFinite => E hfE h. apply: (@Bar_grel_incl _ _ (r_union nR nS)). - apply: Bar_grel_union; last done. by apply: Bar_gpred_grel. move => x y. by move/n_eql2neql. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)