proposition: Lemma sup_wf : forall E, well_founded sup (gpred_list E) -> IFinite eqA E.
proof: Proof. move => E. have: forall X, Acc (gpred_list E) sup X -> gpred_list E X -> IFinite eqA (Intersection E (fun x =>~ (list_to_set X) x)). - move => x. elim => X hacc hi hp; clear x. apply cBar => x0 hx0. apply (@Bar_gset_incl _ (Intersection E (fun x : A => ~ list_to_set (x0::X) x))). case: hx0 => hx1. rewrite /list_to_set; move/negP => hx2. + apply: hi => //=. apply/sub_elim; split. * move => a ha; by apply : InA_tl. exists x0; [by rewrite hx2 | by rewrite InA_hd]. move => a [[h1 h2] h3]. split => //. rewrite /list_to_set /=. case: eqA_dec => //= heq. by move => _; apply: h3; symmetry. move => htemp hwf. apply: (@Bar_gset_incl _ (Intersection E (fun x : A => ~ false))). - by apply: (htemp [::]). by move => a ha. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)