proposition: Lemma tool6 : forall F, IFinite eqA F -> forall X E, Included E (unionl X F) -> E_compat E -> Bar sub (Intersection (gpred_list E) (sub X)).
proof: Proof. move => f. elim => [F hp hi] X E hincl hE. clear f. apply:cBar => Y. case => hpred. move/sub_elim=> [hsub1 hsub2]. case: hsub2 => x0 hx0 heq. have hincl2 : Included E (unionl Y (Intersection F (neq eqA x0))). - move => x hx. have := hincl x hx. case. move => hXx. left. by apply: hsub1. case: (eqA_dec x x0) => h. move=> hF. left. rewrite /list_to_set. by rewrite (InA_eq Y h). move => hF. right. split => //. move => hh; apply: h. by symmetry. apply : (@Bar_gset_incl _ (Intersection (gpred_list E) (sub Y))). apply:(hi x0) => //. have hEx0 : E x0. move/gpred_listP : hpred. by apply. have := hincl x0 hEx0. case =>// hF. move/negP : hx0. by case. move => L. case => [[h1 h2]] h3. by split. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)