proposition: Lemma lemma6 : forall E, E_compat E -> IFinite eqA E -> Bar sub (gpred_list E).
proof: Proof. move => E hE hfE. have h : Bar sub (Intersection (gpred_list E) (sub [::])). - apply : (@tool6 E) =>//. move => x hx. by right. apply cBar => y hP. apply: lemma6_prime2. by apply: wf_sup. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)