proposition: Lemma wf_sup : forall E , E_compat E -> IFinite eqA E -> well_founded sup (gpred_list E).
proof: Proof. move => E hE. have htemp : forall F, IFinite eqA F -> forall X, Included E (unionl X F) -> Acc (gpred_list E) sup X. - move => f. elim => [F hp hi] X hincl; clear f. apply :Acc_intro => Y hpred. case/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 => hu. * left. by apply: hsub1. case: (eqA_dec x x0) => h. * left. by rewrite /list_to_set (InA_eq Y h). right. split => //. move => hh; apply h. by symmetry. apply: (hi x0) => //. have hEx0 : E x0. + move/gpred_listP : hpred. by apply. have := hincl x0 hEx0. case => hu //. move/negP : hx0. by case. move => hE2 X. apply: (htemp E) => //. move => x hx. by right. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)